Semantic Models

In the past 50 years there have been three standard models of programming language semantics

Operational Semantics

The world view of the operational semantics is that programming language meaning can best be transmitted by an agreed upon abstract computer model. Operational semantics were heavily used in the 1960s and 1970s, primarily with the programming language PL/1. The basic criticism of operational semantics is that of infinite regress: there never was a statement which did not have some ambiguity.

Axiomatic Semantics

Axiomatic semantics was introduced by C. A. R. Hoare in the late 1960s and early 1970s. The basic unit of axiomatic semantics is the Hoare triple that we will write as {P}S{Q}. Informally, P is the precondition, S is the statement, and Q is the postcondition. The intent of this approach is to develop a logic similar to that used in ordinary mathematics.

The intuitive reading of {P}S{Q} is "If the state P is true and the statement S is executed, then the state Q obtains." Immediately, the issue arises, "Well, what if S doesn't terminate?" There is no unique answer to this question so there are two different interpretations of {P}S{Q}: (1) if P guarantees that S terminates then we have total correctness and (2) if P does not guarantee that S terminates we have partial correctness.

The major stumbling block with axiomatic semantics is that ordinary assignment is difficult to capture using this notation.

Denotational Semantics

Denotational semantics was originated by Christopher Strachey in the 1960s and 1970s. After Strachey's untimely death, Dana S. Scott continued guiding the development. The worldview of is the lamba-calculus. The lambda calculus is fundamental to logic and was introduced by Alonzo Church in the 1930s. The use of lambda calculus was propularized by John McCarthy through the first functional language, Lisp. The basic concept in denotational semantics is that what a statement means is whatever it computes. The lambda calculus can be used as a sound basis for recursive functions.

The denotational model is comprised of three parts: the concept of abstract syntax trees, the valuation function, and the constructive support algebra.