Flemming Nielson

Indeholder "List of Tables", "1. Introduction", " 1.1 Semantic description methods", " 1.2 The example language While", " 1.3 Semantics of expressions", " 1.4 Properties of the semantics", "2. Operational Semantics", " 2.1 Natural semantics", " 2.2 Structural operational semantics", " 2.3 An equivalence result", " 2.4 Extensions of While", " 2.5 Blocks and procedures", "3. Provably Correct Implementation", " 3.1 The abstract machine", " 3.2 Specification of the translation", " 3.3 show more Correctness", " 3.4 An alternative proof technique", "4. Denotational Semantics", " 4.1 Direct style semantics: specification", " 4.2 Fixed point theory", " 4.3 Direct style semantics: existence", " 4.4 An equivalence result", " 4.5 Extensions of While", "5. Static Program Analysis", " 5.1 Properties and property states", " 5.2 The analysis", " 5.3 Safety of the analysis", " 5.4 Bounded iteration", "6. Axiomatic Program Verification", " 6.1 Direct proofs of program correctness", " 6.2 Partial correctness assertions", " 6.3 Soundness and completeness", " 6.4 Extensions of the axiomatic system", " 6.5 Assertions for execution time", "7. Further Reading", "Appendices", "A. Review of Notation", "B. Introduction to Miranda Implementations", " B.1 Abstract syntax", " B.2 Evaluation of expressions", "C. Operational Semantics in Miranda", " C.1 Natural semantics", " C.2 Structural operational semantics", " C.3 Extensions of While", " C.4 Provably correct implementation", "D. Denotational Semantics in Miranda", " D.1 Direct style semantics", " D.2 Extensions of While", " D.3 Static program analysis", "Bibliography", "Index of Symbols", "Index".

Noget om semantik af programmeringssprog og om Miranda. show less