Operational Reasoning and Denotational Semantics
Abstract
Obviously true properties of programs can be hard to prove when meanings are specified with a denotational semantics. One cause of this is that such a semantics usually abstracts away from the running process - thus properties which are obvious when one thinks about this lose the basis of their obviousness in the absence of it. To enable process-based intuitions to be used in constructing proofs one can associate with the semantics an abstract interpreter so that reasoning about the semantics can be done by reasoning about computations on the interpreter. This technique is used to prove several facts about a semantics of pure LISP. First a denotational semantics and an abstract interpreter are described. Then it is shown that the denotation of any LISP form is correctly computed by the interpreter. This is used to justify an inference rule - called LISP-induction - which formalises induction on the size of computations on the interpreter. Finally LISP-induction is used to prove a number of results. In particular it is shown that the function eval is correct relative to the semantics - i.e. that it denotes a mapping which maps forms (coded as S-expressions) on to their correct values.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1975
- Accession Number
- ADA017176
Entities
People
- Michael Gordon
Organizations
- Stanford University