This project is read-only.

exists comprehension?

Jun 2, 2010 at 10:49 AM

Hi there,

The following class produces the error given below

public class A {
    A?[]! elems = new A[10];
    [Pure] public bool exists(A! node)
    ensures result==exists{int i in (0:elems.Length);elems[i]==node};
    {
    return exists{int i in (0:elems.Length);elems[i]==node};
    }
}

 

Warning   Method A.exists(A! node), unsatisfied postcondition: result==exists{int i in (0:elems.Length);elems[i]==node} 

Surely trivially the postcondition should hold? or am I missing something?

 

Thanks,

Chris Jones

Jun 5, 2010 at 2:47 AM

Good question.  While the Spec# compiler is happy with quantifiers like "exists" in code, the verifier only understands quantifiers in specifications, not in code.  A quantifier in code, like in your return statement above, is compiled into a loop.  The verifier, which starts from the bytecode, sees that loop.  It does not try to decompile the loop or otherwise figure out that it came from a quantifier.  Therefore, it will reason about it like any other loop, which would require a loop invariant (and that loop invariant would need to mention a quantifier...).

See also section 1.3 of the Spec# tutorial, which shows an example similar to yours.

Jun 10, 2010 at 5:04 PM
Edited Jun 10, 2010 at 5:05 PM
Thanks for your reply - that is most insightful. What I don't see, however, is how the following fails to verify: public class Array { [Rep] int[]! a; invariant a.Length==1; public Array() ensures exists{int k in (0:a.Length); a[k] == 0};//a4 { a = new int[1]; a[0] = 0; assert a[0] == 0;//a1 assert a.Length==1;//a2 assert exists{int k in (0:a.Length); a[k] == 0};//a3 } } With the warning: Method Array(), unsatisfied postcondition: exists{int k in (0:a.Length); a[k]==0} I assume this is something to do with it being the constructor of the object, as this method does verify when it is not a constructor. Surely, though, this should verify as well? Am I missing something? Many thanks, Chris (p.s. I am not sure why the line breaks are not coming up on the actual post, making this example difficult to read - apologies!)
Jun 10, 2010 at 8:10 PM

Hi Chris,

There is more to say about your example than I wish there were.  There are several things going on, and at least one of them is new to me.

First, at the end of the constructor, between the last statement of the body and the checking of the postcondition, Spec# adds an operation that checks the object invariant and then changes the state of the object to record that the object is valid for the enclosing class.  That state change sits between your assertion in the body and the identical postcondition.  In this case, this state change stands in the way of the verifier figuring out that the postcondition holds.  You would see the same issue if there had been any other state update there, for example, an assignment to a field, a method call, or the end-curly-brace of an expose statement.

Second, existential quantifiers are hard to work with.  The problem we usually see is that the verifier has a hard time establishing an existential quantifier "from nothing".  In such cases, the user usually has to supply a witness.  You have essentially done that in your program by assigning a[0]= 0; (and also by asserting a[0]==0).

Proving that an existential property is maintained by a piece of code is, I usually argue, on par with proving that a universal property is maintained by a piece of code.  The reason for this is that the prover will negate the quantifier after the code, so it will end up with one universal and one existential quantifier, and that is usually a situation that works well for SMT solvers.  (Trying to prove that a piece of code maintains an alternating quantifier--an exists inside a forall, or vice verse--is a different story, and in those cases, the SMT solver is usually bound to fail.)

The code in this case is essentially a case of maintaining an existential quantifier (from the assert to the ensures), and yet it does not work.  Here, there is a difference between maintaining a universal and maintaining an existential, it seems.  The issue is quite technical and has to do with matching patterns ("triggers").  Our verification-condition generation uses weakest preconditions, which entails that formulas get "more complicated" as they are pushed backwards through the code.  "More complicated" in the sense of accumulating more structure as the VC generation passes over assignment statements and other updates.  In your case, it means that the universal formula at the end (remember, the prover starts by negating the formula it's trying to prove) gets more complicated (to get really technical, it will contain some "store" expressions, which reflect the state update that I talked about above), and this also affects what matching triggers are used by the prover.  Matching a simpler ground term against a more complicated trigger does not seem like a recipe for success.  And that is what happens here.

My best suggestion for this example is that you expose the witness in the program text.  That will make your program a little, though, I'm afraid, but it will work around the problem.  Change your constructor to:

  Array(out int k)
    ensures 0 <= k && k < a.Length && a[k] == 0;
  {  ...  k = 0; ... }

 

Jun 10, 2010 at 9:52 PM

Some more thoughts on this:

In many cases, the recipe for working with existential quantifiers is to manually supply a witness.  The take-home message from the technical details in my previous reply is that such a witness needs to be introduced where you need it, without any intervening state changes.  For postconditions, that usually means you can supply the witness in an assert statement at the end of the method body.  But, because of Spec#'s implicit state change at the end of constructor bodies, you can't do that for constructors, which is where the confusion in the example comes from.

Here is another workaround.  It still makes the code bigger and uglier, but unlike my workaround above, this workaround still hides the existential index from the constructor's callers.

class Array {
  [Rep] int[]! a;
  invariant a.Length==1;

  public Array()
    ensures a != null && exists{int k in (0:a.Length); a[k] == 0};
  {
    int k;
    this(out k);
  }

  private Array(out int k)
    ensures a != null && 0 <= k && k < a.Length && a[k] == 0;
  {
    a = new int[1];
    a[0] = 0;
    k = 0;
  }
}

Note that the second constructor is private.  There is no state change between the "this(...);" call and the and of the public constructor; therefore, the postcondition of the private constructor supplies the witness needed to discharge the existential postcondition in the public constructor.  (The fact that this example needed the "a != null" conjunct in the public constructor, despite the fact that "a" is declared of a non-null type, seems to be a bug in the type checker, but I'm not planning on investigating it further.)