Programming Research Group Research Report RR-02-13

Dan R. Ghica

November 2002, 177pp.

Abstract

We present a program specification language for Idealized ALGOL that is compatible both with inferential reasoning and model checking. Model-checking is made possible by the use of an algorithmic, regular-language semantics, which is a representation of the fully-abstract game semantic model of the programming language. Inferential reasoning is carried out using rules based on Hoare's logic of imperative programming, extended to handle procedures and computational side effects. The main logical innovation of this approach is the use of generalized universal quantifiers to specify properties of non-local objects. Together, the regular-language semantics of the programming language and its specification language on the one hand, and the inferential properties of the specification language on the other provide a foundation for compositional software model checking.