November 2002, 19pp.
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.