Axiom about global variable

Coordinator
Jan 5, 2015 at 6:52 PM
Here is a question I recently received:

I have an axiom:
axiom (forall t : javaType :: $heap[$null,$type] <: t);
where $heap is global. The parser rejects this axiom saying
Error: cannot refer to a global variable in this context: $heap
How would you state such an axiom?
Coordinator
Jan 5, 2015 at 6:57 PM
Axioms are not allowed to have free variables. You have to introduce some predicate on heaps and use it in your axiom. For example:
type HeapType = [Ref, FieldName]: javaType;  /* or whatever the type of your $heap is */
function ReachableHeap(HeapType): bool;
axiom (forall t: javaType, h: HeapType :: ReachableHeap(h) ==> h[$null, $type] <: t);
Note that you do not want to quantify over all values of HeapType without using ReachableHeap, because that would introduce an unsoundness. Consider:
axiom (forall  t: javaType, h: HeapType :: h[$null, $type] <: t);
Now, suppose there is some values X and Y for which it is known that X <: Y does not hold. One could now instantiate the axiom with t := Y and h := (lambda r: Ref, tn: FieldName :: X), and then you can derive false. Suppose $heap is an expression of type HeapType; then another way to derive false would be to instantiate the axiom with t := Y and h := $heap[$null,$type := X].

To make use of this axiom, you must now make sure that the predicate ReachableHeap holds of $heap in every program state. You could introduce
assume ReachableHeap($heap);
after every assignment to $heap (but you may or may not need to, since the assignment RHS will reveal whatever is known about the new value). It’s a bit trickier to also add such an assume after every havoc of $heap, because such havocs are introduced by Boogie when it cuts loop back-edges. Luckily, Boogie has a facility for indicating a predicate that should be assumed after every havoc of a variable (which includes the havoc introduced for loop targets when loop back-edges are cut, and also includes the implicit havoc that is applied to local variables and procedure parameters on entry to procedures, before assuming the precondition, and is applied to the implicit havoc on out-parameters at a call site, before assuming the postcondition). This facility is the where clause. So, to get this assumption for all havocs of $heap, you could simply declare $heap as follows:
var $heap: HeapType where ReachableHeap($heap);
Note, where clauses have no effect at assignments. I believe the Boogie language reference, "This is Boogie 2”, has more information and some example about where clauses.

Rustan
Marked as answer by rustanleino on 1/5/2015 at 11:57 AM