Lecture Formal methods in software engineering - Lecture 17 presents the following content: Semantics, operational semantics, evaluation of operational semantics, axiomatic semantics, axiomatic semantics form, axiomatic semantics - consequence, loop invariant, evaluation of axiomatic semantics. | Formal Methods in Software Engineering Lecture 17 Describing Syntax and Semantics Formal Methods in Software Engineering Semantics How do we describe the “meaning” of a program? Dynamic semantics or semantics is concerned with accurately describing the execution behaviour of a language Why do we care? English descriptions are often incomplete and ambiguous Compiler writers must implement the language description accurately Programmers want the same behaviour on different platforms There is no single widely acceptable notation or formalism for describing semantics Entire books have been dedicated to various semantic notations! Formal Methods in Software Engineering Operational Semantics Describe the meaning of a program by executing its statements on a machine, either simulated or actual. The change in the state of the machine (memory, registers, etc.) defines the meaning of the statement At the highest level, we’re interested in the final result (natural operational semantics) At the lowest level, look at a translated version to determine precise meaning of a single statement (structural operational semantics) Formal Methods in Software Engineering Operational Semantics Example C Statement for (expr1; expr2; expr3) { . . . } Operational Statements expr1; loop: if expr2 == 0 goto out . . . expr3; goto loop out: . . . Human reader is virtual computer, assumed to be able to correctly “execute” the instructions and recognize the effects. Note that language is intermediate level, not machine language. Formal Methods in Software Engineering Operational Semantics (continued) A better alternative: A complete computer simulation The process: Build a translator (translates source code to the machine code of an idealized computer) Build a simulator for the idealized computer Formal Methods in Software Engineering Evaluation of Operational Semantics Good if used informally (language manuals, etc.) Extremely complex if used formally . | Formal Methods in Software Engineering Lecture 17 Describing Syntax and Semantics Formal Methods in Software Engineering Semantics How do we describe the “meaning” of a program? Dynamic semantics or semantics is concerned with accurately describing the execution behaviour of a language Why do we care? English descriptions are often incomplete and ambiguous Compiler writers must implement the language description accurately Programmers want the same behaviour on different platforms There is no single widely acceptable notation or formalism for describing semantics Entire books have been dedicated to various semantic notations! Formal Methods in Software Engineering Operational Semantics Describe the meaning of a program by executing its statements on a machine, either simulated or actual. The change in the state of the machine (memory, registers, etc.) defines the meaning of the statement At the highest level, we’re interested in the final result (natural operational .
