| |
K. Rustan M. Leino and Rajit Manohar
The specification statement allows us to easily express what a program
statement does. This paper shows how refinement of specification
statements can be directly expressed using the predicate calculus. It
is also shown that the specification statements interpreted as
predicate transformers form a complete lattice, and that this lattice
is the lattice of conjunctive predicate transformers. The join
operator of the lattice is directly expressed as a specification
statement. The join operator of two interesting sublattices of the set
of specification statements is also investigated.
|
|
