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
havoc s are introduced by Boogie when it cuts loop backedges. 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 backedges 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 outparameters at a call site, before assuming the postcondition). This facility is the
where clause. So, to get this assumption for all havoc s 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
