Joining Specification Statements

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.