Does Danfy have global quantified expressions?

Jan 18, 2013 at 1:47 AM
Edited Jan 18, 2013 at 3:44 PM

[[ Sorry that  the title is confusing.  "global quantified" should be "universally quantified". I did not find a way to revise the title.]]

I am wondering if Dafny has universally quantified expressions. For example

int m()

forall b: int;

requires valid(b);

ensures valid(b + amount);

{

}

which corresponds to the Hoare triple:

\forall b. { valid(b) } m() { valid(b + amount) }.

And how to encode it into boogie?

 

Thanks

Yuyan

Jan 23, 2013 at 11:52 AM
Edited Jan 23, 2013 at 11:53 AM

In Dafny, suppose i have a method void m(int) and a predicate valid(int), such that:

void m(amount: int)

requires valid(this.b);

modifies this;

ensures valid(old(this.b) + amount);

{

 ...

}

Putting the frame problem aside, I think to verify this method, Boogie assumes an arbitrary value of this.b that satisfies the predicate valid, then checks if it is satisfies the postcondition.

If so, may I consider it as "universally quantified"?

Does it amount to

requires this.b |-> ?v &*& valid(v);

ensures this.b |-> v + amount &*& valid(v + amount);

in symbolic verification tool, such as VeriFast?

Jan 26, 2013 at 1:33 AM

I think the meaning of

requires valid(this.b);  

is

assume valid(this.b);

The meaning of 

requires this.b |-> ?v && valid(v);

is

var v: int; (suppose this.b has type int)

havoc v;

assume valid(v) && this.b == v;

Hence, the two precondition can consider as equivalent. Am I right?

Coordinator
Jan 30, 2013 at 8:55 PM
Hi Yuyan,

The kind of variables you're talking about are often called "logical variables". There are necessary in Hoare logic when you want the postcondition to refer back to the pre-state. For example, to express that a statement S increments a variable x, you would write:
{ x = X }    S    { x = X+1 }
where X is such a logical variable. When you verify S to satisfy this Hoare triple, the value of X is arbitrary, so you have to prove that S satisfies the Hoare triple for all possible values of X -- this explains why you may refer to them as "universally quantified". Note, however, that things are reversed when you reason about a call to S (or "use of S", if S is not a procedure). For example, suppose you want to verify the Hoare triple
{ true }    x := 17;  S    { x = 18 }
Then you have to "instantiate" the specification of S with 17 for X. So, the caller first needs to prove the existence of such an X (or otherwise the call to S is not allowed, assuming a flavor of Hoare semantics that insists that preconditions hold at all call sites), and then the postcondition the caller gets to assume after the call is the disjunction over all X that satisfy the precondition.

This business with logical variables seems like a complicated way to workaround the fact that standard Hoare logic does not have two-state postconditions. If it did, you'd probably just write the specification of S as:
{ true }    S    { x = old(x) + 1 }
Anyhow, VeriFast has logical variables and you use them as you've shown in the example above (with the "?" syntax). VeriFast uses separation logic, which draws much influence from Hoare logic, so logical variables are the way to let your postcondition refer to your pre-state.

In Eiffel, JML, Spec#, Dafny, and Chalice, for example, you have the "old" construct. So, if what you're trying to express in Dafny is just a postcondition that mentions the pre-state, then the easiest way to do that is to use the "old" construct.

If you do want to more directly model logical variables in Dafny, then you can use a field like "this.b" above. If the only purpose for having this field is to write specifications like the above, then you probably want to declared the field to be a "ghost". Note that if you're using a field (or ghost field), you have to worry about the possibility of "this.b" being mutated by the method (in which case you may need to write "old(this.b)"). I think it's easier to, instead of using a field, use an extra parameter to the method. Again, you'd probably want to make the parameter a "ghost". So, for your example, you could write:
method M(ghost b: int)
    requires Valid(b);
    ensures Valid(b + amount);
When you verify the method, things are as you describe above. That is, given that b is an arbitrary value that satisfies the precondition, you have to prove that the body of the method establishes the postcondition (for the same b). Declaring b as a parameter (or as a field, for that matter) puts a burden on the caller to supply a value of b that satisfies the precondition. An advantage with having the caller supply a particular value for b is (that is simplifies the programming logic and) that the caller now gets to assume the postcondition for that particular b (not for the disjunction over all b's that could have satisfied the precondition).

When VeriFast considers a caller, it will supply a value for ?v automatically (and arbitrarily, so long as the value it picks satisfies the precondition). The Chalice tool (which does not have logical variables in general, but instead supports the "old" construct) has a special kind of logical variable that can be used to conveniently specify fractional permissions (see the VMCAI 2013 paper "Fractional permissions with the fractions" by Heule, Leino, Müller, and Summers).

One more thing. Boogie actually supports logical variables, as implemented by Zhaozhong Ni. To set them up, declare a parameter like "b" above (noting that Boogie makes no distinction between ghosts and non-ghosts since Boogie is not a compiled language) and then, on the caller side, pass in the actual parameter as "*" instead of some value. Boogie will then check, using the recipe I mentioned above, that there exists a value for b at the call site, and the caller then gets to assume the disjunction of the postcondition for all b's that satisfy the precondition.

I hope this helps.

Rustan
Feb 1, 2013 at 5:00 PM
Hi Rustan,

That's REALLY helpful! THANKS A LOT!!!

Yuyan