I'm trying to statically verify the following partial implementation of an array-based stack with code contracts. The method Pop()
uses the pure function IsNotEmpty()
to ensure that the subsequent array access will be at/above the lower bound. The static verifier fails and suggests that I add the precondition Contract.Requires(0 <= this.top)
.
Can anyone explain why the verifier cannot prove the array access is valid with respect to the lower bound given the contract IsNotEmpty()
?
At first I thought the Contract.Requires(IsNotEmpty())
approach might be incorrect because a subclass could override IsNotEmpty()
. However, the verifier still can't prove the array access is valid if I mark the class as sealed
.
Update: If I change IsNotEmpty()
to a read-only property, the verification succeeds as expected. This raises the question: how / why are read-only properties and pure functions treated differently?
class StackAr<T>
{
private T[] data;
private int capacity;
/// <summary>
/// the index of the top array element
/// </summary>
private int top;
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(data != null);
Contract.Invariant(top < capacity);
Contract.Invariant(top >= -1);
Contract.Invariant(capacity == data.Length);
}
public StackAr(int capacity)
{
Contract.Requires(capacity > 0);
this.capacity = capacity;
this.data = new T[capacity];
top = -1;
}
[Pure]
public bool IsNotEmpty()
{
return 0 <= this.top;
}
public T Pop()
{
Contract.Requires(IsNotEmpty());
//CodeContracts: Suggested precondition:
//Contract.Requires(0 <= this.top);
T element = data[top];
top--;
return element;
}
}