CSE 505 -- Rough Notes on Formal Semantics

Syntax: structure of a language
Semantics: its meaning

BNF is almost univerally used for specifying the syntax of a language. BNF describes context-free grammars -- which isn't sufficient to capture requirements such as declaration before use. These are often specified informally via a programming language report, and checked in a semantic checking phase of a compiler. Another technique is using attribute grammars or the like to capture semantic checks.

Kinds of semantics

Static semantics: the static properties of the program

main example: typechecking rules

Dynamic semantics: the dynamic behavior of the program

when you run the program, what result do you get?
often defined only for programs for which the static semantics is defined (i.e. those programs that typecheck)

Some flavors of dynamic semantics:

operational semantics
- specified as evaluation steps as by a machine
- simple, easy to build an interpreter from
denotational semantics
- specified directly in terms of mathematical functions
- more abstract than operational semantics
axiomatic semantics
- specified via pre- and post-conditions
- good for doing behavioral specification & correctness proofs

Operational Semantics

The operational semantics of side-effect-free languages such as CLP languages or pure functional languages is almost invariably defined using rewriting rules. This produces a very clean description, which lends itself to a direct implementation strategy. Optimizations may be important for efficiency, but we normally want them to preserve meaning, that is, any optimized program should produce the same results as an unoptimized one.

For CLP languages, derivation trees are the standard way of providing an operational semantics. A derivation step (remember from CLP?) is a rewrite rule, rewriting a state <G0|C0> to another state <G1|C1>

For functional languages, rewriting is again the standard way of providing an operational semantics. See separate handout on Applicative vs Normal Order Evaluation in Functional Languages.

An operational semantics for an imperative language will generally be more complex, due to the need to account for state. Some interesting examples include the Smalltalk byte code definitions and the Lisp meta-circular interpreter (Lisp written in Lisp).

Axiomatic Semantics

In axiomatic semantics we formally specify predicates that hold before and after execution of a statement. Statements are defined by how they modify these relations.

We will write

{P} S {R}

to mean "if predicate P is true before program S starts, and S terminates successfully, then R will be true after S terminates."

Examples (taken from Raphael Finkel, "Advanced Programming Language Design"):

Axiom of assignment

{P[x->y]} x := y {P}
where
       x is an identifier
       y is an expression without side effects, possibly containing x

{P[x->y]} means the predicate P with all occurrences of x replaced by y.

Examples:

If we want x>0 to be true after the execution of x := y then y>0 must be true before the execution of the assignment.

If we want x>1 to be true after the execution of x := x+1 then x+1>1, in other words x>0, must be true before the execution of the assignment.

Caution: the axiom of assignment does not hold in the presence of aliasing!!

Axiom of composition:

if {P} S1 {Q} and {Q} S2 {R} then {P} S1; S2 {R}

Axiom of iteration:

if {P and B} S {P} then
   {P} while B do S end {not B and P}

We can have pre- and postconditions of various strengths. The strongest possible condition is false (it doesn't hold for any program state). The weakest possible condition is true (it holds for any program state). Examples:

{true} S {false}

holds only for non-terminating programs.

{false} S {true}

holds for all programs.

Weakest precondition. What is the weakest precondition for a program for a given postcondition?

Denotational Semantics

We'll cover this on the whiteboard, working from the Tennent paper.