Figure 4: The Verification-Condition Generator.
To compute the safety predicate, we first generate a vector 
of
predicates, one for each instruction as specified by the rules in Figure 4.
The notation 
denotes the predicate for the current instruction.
Since the rules specify 
in terms of 
, the
verification-condition 
for the beginning of the program can be computed
by starting at the end of the program and working back towards the
beginning.
The rules in Figure 4 are derived in a straightforward manner from the
abstract machine specification of abs-mach; in fact, we imagine
that experienced kernel and safe-ty policy designers would skip the abstract
machine specification and give only the VC generator rules.
The notation 
stands for the predicate
obtained from P by substituting 
for 
.
After computing the vector 
, the safety predicate is computed simply
by plugging the program 
, precondition 
, and postcondition
into the following formula:
The intuition behind a valid safety predicate is that for any initial state
that satisfies the precondition 
, the code 
starting at the first
instruction executes without failure and, if it terminates, the final state
satisfies the postcondition 
.
For a concrete example of client code for the resource access service, consider
the small program in ex-code. The overall effect of this program is to
increment the data word if it is writable. We first compute 
for this
program using the rules in Figure 4; then we compute the safety predicate
using the above formula with the precondition 
and the
postcondition . After a few trivial simplifications, the resulting safety
predicate is the following:
Informally, the 
predicate says that for all values of register 
and states of memory 
satisfying the precondition 
, the
memory locations 
and 
must be readable and if the tag (at
address 
) is non zero, the data (at address 
) must be writable.
All these conditions must be true for the code to be safe with respect to the
resource access safety policy.