I've been attempting to write preconditions and post-conditions for the "Heapify" method for a Min Priority Queue.

Anyways, like the title says, I would like to say something like this in my requires clause:

private void Heapify(int i)

requires 1 <= i && i <= Max_Length;

requires forall{ int j in (i+1: Size); if (2*j <= Size) then Data[j] < Data[(2*j) && if ((2*j)+1 <= Size) then Data[j] < Data[((2*j) + 1)]};

ensures forall{ int j in (i: Size); if (2*j <= Size) then Data[j] < Data[(2*j) && if ((2*j)+1 <= Size) then Data[j] < Data[((2*j) + 1)]};

{ ... }

Note the presence of the if-then.

Is this currently possible to do this with spec#?

I'm using a fixed-size array to represent my heap, however, in order to access the left and right children from any possible index, I'm using the typical 'formula' of 2*index and (2*index) + 1. The reason this ends up being an issue is because - during a typical call to heapify - it is commonly the case where  index * 2 or index*2+1 outsteps the bounds of Size (an instance variable of my Queue class that describes how much the user has inserted into the array) the actual heapify code handles this though. While there is legitimate data in the array at indices > Size, I want to ignore them since they are no longer part of the heap. Anyways, without that "if" check the verifier - rightfully so - picks up on failed conditions entering heapify since I am not trying to guarantee that anything greater than size is a valid min heap. 

Hi!

syntactically there is no if-then construct in Spec#. However, the implication operator (==> in Spec#) can be used here. The following code should verify:

class Heap {
  int[]! Data = new int[10];
  int Size;
  invariant Size <= Data.Length;

  private void Heapify(int i)
    requires 1 <= i && i <= Data.Length;
    requires forall{ int j in (i+1: Size); ((2*j <= Size) ==> Data[j] < Data[2*j]) && (((2*j)+1 <= Size) ==> Data[j] < Data[((2*j) + 1)]) };
  {}
}

Best regards,

Valentin