I've been attempting to write preconditions and postconditions 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 ifthen.
Is this currently possible to do this with spec#?
I'm using a fixedsize 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.
