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