Semantics with applications : a formal introduction
著者
書誌事項
Semantics with applications : a formal introduction
（Wiley professional computing）
J. Wiley, c1992
大学図書館所蔵 全8件
注記
Includes bibliographical references (p. 233-234) and indexes
内容説明・目次
内容説明
The purpose of this book is to present the fundamental ideas behind operational, denotional and axiomatic semantics; stress their relationship by formulating and proving relevant theorems; and to illustrate the applicability of formal semantics as a tool in computer science. The bulk of the text concentrates on a small core language of while-programs for which the three approaches are developed to roughly the same level of sophistication. To demonstrate the applicability of formal semantics, the authors show how to use semantics for validating prototype implementations of programming languages; how to use semantics for verifying analyses used in more advanced implementations of programming languages; and how to use semantics for verifying useful program properties including information about execution time. The reader should have some experience of functional programming and the BNF-style of specifying the syntax of programming languages.
目次
- 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.
「Nielsen BookData」 より