Quantification

Spec# and JML both support quantification operators like forall and exist as seen in lines 9 and 10 of this Spec# code sample:

   1:  class ArrayList { 

   2:  void Insert(int index , object value)

   3:      requires 0 <= index && index <= Count

   4:          otherwise ArgumentOutOfRangeException;

   5:      requires !IsReadOnly && !IsFixedSize

   6:          otherwise NotSupportedException;

   7:      ensures Count == old(Count) + 1;

   8:      ensures value == this[index ];

   9:      ensures Forall{int i in 0 : index ; old(this[i]) == this[i]};

  10:      ensures Forall{int i in index : old(Count); old(this[i]) == this[i + 1]};

I don’t actually directly support quantifiers in the reasoning system used by NStatic. However, because the system completely support functions, quantifiers are actually redundant; I can reduce quantifiers to equivalent unquantified functional expressions.

The most common use of quantifiers seems to be iterating over all elements of an array. In such cases, quantifier keywords can be imitated by C# language constructs.

For the expression Forall{int i in index : old(Count); old(this[i]) == this[i + 1]} from the above code.

     for (int i = index; i < oldCount; i++)
           Debug.Assert(oldArray[i] == newArray[i+1]);

Alternatively and equivalently, the same test could be rewritten as a function called inside of an Assert statement.

    bool TestArray(int[] oldArray, int[] newArray, int index, int oldCount)
    {
        for (int i = index; i < oldCount; i++)
            if (oldArray[i] != newArray[i+1])
                return false;
        return true;
    }

    Debug.Assert(TestArray(oldArray, newArray, index, oldCount);

In the first case, the Assert statement was inside the loop and, in the second case, it was left outside. In either case, they both perform the same operation and are, therefore, normalized to same internal representation.

This illustrates the basic operation of NStatic. Within the limits of the simplifier inside NStatic, straightforward, equivalent fragments of code are normalized to the same representation, regardless of constructs used.

We could define quantification operators more generally as higher-order functions:

[Conditional("CODEANALYSIS")]
bool ForAll(int start, int end, Func<int, bool> predicate)
{
     for (int i = start; i <=end; i++)
           if (!predicate(i))
                 return false;
     return true;
}

[Conditional("CODEANALYSIS")]
bool ThereExists(int start, int end, Func<int, bool> predicate)
{
     for (int i = start; i <=end; i++)
           if (predicate(i))
                 return true;
     return false;
}

Debug.Assert(ForAll(i, index, oldCount-1, 
     delegate(int i) { return oldArray[i] == newArray[i+1]; });

Other types of quantifiers could also be created this way such an existential uniqueness operator. The initial release of NStatic though will probably not have enough simplifications to enable these other quantifiers, due more to lack of time rather than any implementation difficulties.

I inserted the "Conditional" attribute is there simply to avoid compilation into code. Otherwise, the C# compiler would happily compile the code and, if the difference between start and end happened to be a large value like int.MaxValue, the runtime execution of this code could hang for a long time.

NStatic doesn't execute recursive functions and loops, unless such expressions are determined to terminate in a short amount of time and space. Instead, NStatic evaluates loops and recursive functions symbolically by recognizing patterns in the loop and simplifying them, allowing its analysis of the same expression to proceed quickly.  The simplified representation of the loop is then used as its value.

For quantifying over non-indexable sets, we could have functions over collections or functions that walk through composite data structures. To quantify over all the objects in the heap, though, it would seem we may need a special quantifier keyword or class invariants, which I won't be adding until support for specifications in a future version.

Comments

[Chris]

Does Spec# work well now? I tried it a few months ago, and it would sometimes compile or come up with errors (with the very exact same code!)

The randomness drove me crazy and I haven't touched since.

BTW, is NStatic downloadable, or closed beta?

I tried looking for a link but couldn't find it.

Chris

[Wesner Moise]

None of these code blocks have actually been tested.

I should point out that because the function is called and used within the Debug.Assert, the Conditional attribute may still not prevent the code from avoiding compilation.

[Wesner Moise]

Chris, it's neither beta or downloadable yet. I have people close to me helping me.