Semantics With Applications: A Formal Introduction

Part 1 Introduction: semantic description methods the example language While semantics of expressions properties of the semantics. Part 2 Operational semantics: natural semantics structural operational semantics an equivalence result extensions of While blocks and procedures. Part 3 Provably correct implementation: the abstract machine specification of the translation correctness an alternative proof technique. Part 4 Denotational semantics: direct style semantics - specification fixed point theory direct style semantics - existence an equivalence result extensions of While. Part 5 Static program analysis: properties and property states the analysis safety of the analysis bounded iteration. Part 6 Axiomatic program verification: direct proofs of program correctness partial correctness assertions soundness and completeness extensions of the axiomatic systems assertions for execution time. Part 7 Further reading. Appendices: Review of notation introduction to Miranda implementations - abstract syntax evaluation of expressions operational semantics in Miranda - natural semantics structural operational semantics extensions of While provably correct implementation denotational semantics in Miranda - direct style semantics extensions of While static program analysis.