Programming Research Group Research Report RR-02-14

Dan R. Ghica

November 2002, 19pp.

Abstract

We are presenting a semantic analysis of Reynolds's specification logic of Idealized ALGOL using the operationally-based techniques developed by Pitts. We hope that this more elementary account will make the important insights of Tennent and O'Hearn, originally formulated in a functor-category denotational semantics, more accessible to a wider audience. In addition, the operational model gives simple proofs to new axioms of specification logic as well as an interesting non-decidability result.