Semantics with Applications
A Formal Introduction
Published on 6. December 1991
Book
Hardback
252 pages
978-0-471-92980-2 (ISBN)
Description
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.
More details
Language
English
Place of publication
Chichester
United Kingdom
Publishing group
John Wiley and Sons Ltd
Target group
College/higher education
Professional and scholarly
Illustrations
tables, further reading, bibliography, index
Dimensions
Height: 244 mm
Width: 166 mm
Weight
490 gr
ISBN-13
978-0-471-92980-2 (9780471929802)
Copyright in bibliographic data is held by Nielsen Book Services Limited or its licensors: all rights reserved.
Schweitzer Classification
Persons
Content
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.