Formal semantics
math :: theory of computation :: terms
Formal semantics describes concepts and provides us with technics to build mathematical models of programming languages upon which we can conduct various analysis, using them as a focal point in reasoning about programs' behaviour.
The semantics of PL is often divided into 3 sections:
Operational semantics describes the meaning of a PL by specifying how it executes on a VM. Evaluation and execution relations are specified by syntax driven rules. It was advocated by Gordon Plotkin as structural operational semantics.
Denotational semantics is a technique for defining the meaning of PL with mathematical concepts of complete partial orders, continuous functions and least fixed points. Also known as the mathematical semantics, it was pioneered by Christopher Strachey and provided with a mathematical foundation by Dana Scott.
Axiomatic semantics puts emphasis on the proof of correctness by issuing rules, intended to constrain a PL construct, within the program logic. For example, placing conditions that assert a PL construct is behaving as expected. The principle form of this approach, called Hoare logic, is named after its creator, C.A.R. Hoare.
Last updated