How do we determine that a program is correct? Testing won't do it -- testing only demonstrates that it works for the particular cases tested. An alternative -- use mathematical logic to PROVE that the program is correct for all cases.

In 1967, Robert Floyd developed a technique to relate any computer program to a series of logical assertions. Each assertion is true whenever "control" passes it. The assertions are tied together by statements in some programming language that appear between the assertions. Hopefully, the entry assertion states the conditions under which the program will run, and the exit assertion describes what the program computes. This approach was adapted by C. A. R. Hoare a few years later into an axiomatic approach to defining the semantics, or meaning, of every statement in a programming language. This forms one of two methods used to define language semantics.

To apply to all programs, the method is defined for a general "flowchart language", into which the statements of programming languages are to be compiled. The language contains "boxes", linked by flow-of-control arrows.

Here, x is a variable, and v represents a vector consisting of all the variables in the program. f(x,v) is some function or expression of x, and the other program variables, while P, Q, and R are predicates computed on all the variables of the program. If assertion P is true on entry to a flow-arc, and Q must be true at its arrow-tip, then you must prove that P implies Q for the labeling by assertions to be valid. The proof of the program's correctness consists of attaching assertions that fit the flow-box axioms above to the flow-arcs. These assertions must be chosen carefully, so that they allow the flowchart to be verified, and so that the entry and exit assertions serve to describe the program's desired entry and exit conditions.

Example: Compute S = sum{A[i] | i=0..N-1}.

We know that sum{A[i] | i=1..j} = sum{A[i] | i=1..j-1} + A[j], as a property of the summation operation.

To define the semantics of a programming language, one uses the technique above to derive "verification conditions" for each statement of the language. These conditions are stated by giving a rule like: {P}st{Q} for each statement-form "st" of the language. To determine the meaning of a program in the language, one decorates the "gap" between each statement with an assertion, and then checks that assertions bordering statements satisfy the verification conditions for those statements. For a simple language (subset of C) we have:

{S(f(x,v),v)} x = f(x,v); {S(x,v)}

{ P & B} S { Q } and { P & ~B } T { Q } è { P } if B then S else T { Q }

{ P & B } S { P } è {P} while (B ) S { P & ~B }

P implies Q & { Q } S { R } è { P } S { R }

R implies T & { Q } S { R } è { Q } S { T }

These axioms are often given in the form of "weakest pre-condition" rules: {wp(S, P) } S { P }. The assertion wp(S,P) is the "weakest" assertion that can be made prior to statement S that forces assertion P to be true after S finishes execution. By "weakest", I mean that every other assertion T that could be true before S to force P to be true after S satisfies T implies wp(S, P). By inserting an assertion at the end of a sequence of statements (for example, the end of a loop body), one can use "weakest precondition" axioms to produce the weakest assertion that must be know at the beginning of the sequence, for the final assertion to hold. However, when using this approach on a while statement, you should note that there is more to it than simple substitution. Given that Q must be true after the loop, one must invent the "invariant" P that appears in the while axiom, so that (a) the axiom can verify the loop, (b) the entry conditions imply P, and (c) P implies Q.

For complex programs, deriving the invariant for each loop is error-prone, and tedious. Programming languages have been developed to allow assertions to be inserted manually into code, and in some cases checked for correctness automatically (although that requires use of an automatic theorem prover ). People have also advocated developing the program and the proof together. The hope that mathematical proof techniques could serve to ensure that software is bug-free hasn't materialized. The problem seems to be that in real mathematics, published proofs always "skip" steps. Eventually those proofs are accepted when many mathematicians examine the proof, looking for ways to improve it, or falsify it. Unfortunately the theorems derived from programs are apparently so uninteresting that this community of people examining the proofs does not exist.

The idea that a program can be argued to be correct by decorating it with assertions is used to assist in documentation, and in various software methodologies, like the structured walkthrough, which concentrate on program correctness. As a result, interest in using this approach to define the meaning of a programming language has waned somewhat.

To define the meaning of a language L, one needs rules which allow one to "know" what each program in the language computes. One way to get such rules is to give a program written in a well-understood language W to represent in some way what every statement of language L does. The most accurate way to do this is to write an interpreter for L in W. This approach is termed "operational" semantics. The LISP interpreter (written in LISP) is an attempt at this. It fails, because it relies on the reader's already knowing some LISP. So the problem arises: what should the language W be.

One could choose C as W. However, C is large, not type-safe, and isn't itself completely defined in a formal sense. One is looking for a "language-neutral" semantic definition, one that is not biased to make some programming concepts easy to define, while others, no harder to understand, are nearly impossible to define.

Arguably, programs compute mathematical functions. One could define the meaning of a program, by giving mathematical definitions which together define precisely what function the program computes.

To do this, one needs to develop mathematical schemes which model most of the operations one finds in real programs. These schemes must be precisely defined, and must give answers that agree with those real programs (which are known to be correct) actually produce.

Denotational Semantics develops these mathematical schemes.

One defines Semantic Functions which map language features into mathematically precise objects. As an example, the meaning of a binary integer constant BN can be defined, first by giving the abstract syntax of the written form of the constant, and then by showing how any written form, corresponding to that abstract syntax, can be operated on to produce an appropriate mathematical integer:

Syntax:

BN in BinLit
BN è 0 | 1 | BN 0 | BN 1

Semantics:

Semantic domain: N = { 0, 1, 2, ... } (the set of mathematical integers, over which standard operators +, -, *, / are defined)

Semantic function:

E : BinLit è N

E[0] = 0
E[1] = 1
E[BN 0] = 2*E[BN]
E[BN 1} = 2*E[BN] + 1

In attempting to give mathematical meanings to the various operators of a language, one finds need for more complex sets of things than the integers. These sets are termed semantic domains. Semantic domains are either "basic" (predefined in ordinary mathematics), or are constructed: Product domains D=D1 Ä D2 (ML tuples with 2 components), Function domains F=D1è D2, which map elements of domain D1 to elements of domain D2 (ML functions of one argument), and Disjoint Union domains D=D1Å D2, which are set unions, but with each element "tagged" with the source domain from which it came. D = { (1, x1) | x1 in D1 } È { (2, x2) | x2 in D2 }. Such a disjoint union is like an ML datatype. Some special notation is useful:

Suppose f Î D1 è D2, x1 Î D1, and x2 Î D2, then f[x1 ¬ x2] denotes a new function f', defined so that
f'(x) = if x=x1 then x2 else f(x). Function domains are used to map, among other things, arrays. This ability to define a new function which differs from an old one at just one point makes this use convenient.

One can systematically augment each domain, to make new domains which behave more like computer-computed results. For instance, the definition of division involves specifying what the result of dividing by 0 is. One can introduce notation to represent an "error value" ^ and introduce a domain R = N È { ^ }, so the domain of division can be properly specified. One can also use this value to represent the result of an arithmetic operation that overflows.

The text defines Identifiers (a syntactic domain), along with a lookup function that returns the current value of the identifier, which can be a Bool, and integer or udef (if this identifier is not defined). Next, programmer-defined environments are introduced, where an environment is a function that maps identifiers into results. U is the domain of environments, where U=Id è V and V=NÅ BoolÅ {udef}Å {^ }. The development proceeds by adding ways to build a sequence of environments, by adding declarations, mappings that add variables to environments (by point-wise redefining the identifier lookup function, say), extensions for arrays, and means for evaluating an expression in an environment. If desirable, one can define memory as a mapping from integer locations to values (typed, of course), and change the definitions of variables into references to this memory, in case one has to model the finiteness of memory, and the forms of declarations that allow parts of an array to overlap several other arrays (FORTRAN EQUIVALENCE), or reference specific absolute memory locations (C ).

This buildup of definitions serves to handle most statement sequences, but special care must be taken when defining the meaning of a while loop. The problem is that such a loop may never terminate. The desired definition should be ^ if the loop does not terminate, and otherwise will be some new environment (in which new variable definitions apply). Denotational semantics uses an approach based on limits to derive the appropriate definition:

S[while T do St] u represents the result of evaluating a while statement in environment u.

S[while T do St] u = lim _{i® ¥} r _i(u), where r _i+1(w)=if E[T]w then r _i(S[St]w) else w.

The notation E[T]w means "compute E[T], the mathematical function which evaluates expression T. Apply that function to environment w, and return the result, a value". The text decorates this basic expression with extra tests to ensure type compatibility, and to return ^ if E[T]w yields that value. Similar care is needed in defining the evaluation rules for recursive functions.

The attempt to develop means to ensure programs are correct is laudable. I'd like to be able to buy software which comes with a guarantee that it will do a certain job, if started with specific defined input conditions. There also ought to be a formal definition given of what the programming language says my program will do, and hence what any program written in that language "means". Denotational semantics defines meaning by essentially translating the program into mathematical functions. It is somewhat biased toward a functional style of programming, although its elaborate series of definitions allows variables, and even arrays and iteration. Denotational Semantics is actually modeled very well by SML -- or maybe I should say that SML is modeled closely on DS. As a practical matter, one could define a new language's semantics in DS, define an interpreter for DS, and produce a running interpreter for the new language "automatically" (as soon as you have worked the bugs in the semantic definitions out). This, however, does not solve the problem of program correctness -- the DS definitions map a source program that computes the wrong answer into a DS program that computes the same wrong answer. Axiomatic semantics, combined with programming standards that require a programmer to produce a proof that her/his program is correct would be needed, to solve the correctness problem. Given the time pressures on the production of software, this isn't likely to happen soon.

Page 366 in the text lists a number of "tenets" of good programming practice that have developed as a direct result of the efforts to use axiomatic semantics to prove programs correct. The final paragraph of section 10.2.2 on that page also mentions some of the reasons why people do not expect to see such proofs.

Page 419-420 (all of section 10.4) summarize the author's conclusions about Denotational semantics. The last 3 paragraphs are of particular interest.