Goals
Giving a formal or mathematical version of documentation reveals obscurities,
ambiguities, complexities, and impossibilities in apparently clear documents.
The formal documentation forms a reliable and clear basis for implementation
and verification of the object documented. Mathematical documentation is also
the basis for the analysis of the thing being documented and predicting its
properties.
These uses of general formal specification have proved true when used to
define the syntax of programming languages. All programming language syntax
are described by:
- (1) informal description and motivation
- (2) some examples
- (3) the EBNF or some syntax diagrams
However programming language semantics is not defined like this, research has
not demonstrated that there is a uniquely better notation (like EBNF) and
theory(context free grammars). Semantics is still a challenging area. It
demands more complicated mathematical machinery than syntax. Indeed, of all
areas of formal specification, programming languages need the deepest
mathematics.
In Semantics we take the syntax as given and attempt to write down rules that
let us assign a "meaning" to syntactically correct pieces of a language.
Typically we describe the syntax in a BNF-like form. The goal is then to use
this to provide the structure the semantics as well. For example if we define
binary numbers by this XBNF grammar
- Num::= "0" | "1" | Num "0" | Num "1"
We would probably define the meaning as a map N from Num into the
integers including 0:
- N::Num->{0,1,2,3...},
- N("0")=0,
- N("1")=1,
- N(n "0")= 2* N(n),
- N(n "1")= 2* N(n) +1.
Notice that we have one semantic rule for each alternative syntax
so we can be sure that we have defined a meaning for all numbers
constructed according to the syntax of Num. As long as we trust
the recursive rules to terminate.
So for example:
- N("0101")=
- 2*N("010")+1=
- 2*(2*N("01"))+1=
- 2*(2*(2*N("0")+1)+1=
- 2*(2*(2*0)+1)+1= 2*(2*0+1)+1 = 2*(0+1)+1 = 2*1+1 = 3.
Here are the main ways of defining semantics:
Denotational semantics
The meanings assigned to constructs are modeled as mathematical objects that
lie in a particular kind of "space". The objects represent the effect of
Axiomatic Semantics
Here specific properties of the effect of executing the constructs are
expressed as assertions. This ignores even more details. The traditional
form is to use Hoare Triples: {Before}Construct{After}. The Before condition
is called a precondition and the After is a post-condition. Dijkstra has
pioneered a newly popular Calculational approach where for each Construct and
possible After you want the weakest (most general, loosest) precondition is
defined.
Operational Semantics
The meaning of a construct is specified by the computation it induces when it
is executed on a machine. It focusses on how the computation is produced.
However this is (nowadays) in abstract and not on any real of theoretical
machine.
Structural Operational semantics
This describes the meaning in terms of the step by step changes the initial
and final states of the computation.
Natural Operational semantics
This is more abstract and in terms of the overall effect rather than the
single steps.
. . . . . . . . . ( end of section Operational Semantics) <<Contents | Index>>
executing the construct however.
. . . . . . . . . ( end of section Types of Semantics) <<Contents | Index>>
Syntax
- sequence::=statement | statement ";" sequence.
- statement::=assignment.
- assignment::= variable ":=" expression.
- expression::= variable | constant.
Informally we have:
Net
- The state of the program is described by a function that records the value currently assigned to each variable.
- To execute a sequence, execute them one at a time from left to right.
- To execute an assignment, determine the value of the expression and attach it to the variable.
- The value of a constant is itself and the value of a variable is the value assigned to that variable
(End of Net)
We use the following formula to express that S changes state s to
get s':
- <S,s>=>s'.
Similarly,
- <S1,s1>=><S2,s2>
shows that the first step of executing S1 in state s1 is to change state s2
and continue with S2 next.
To reason out the effect of
- <S1;S2;S3..., s>
For example:
- < z:=x; x:=y; y:=z, [ x+>5 | y+>7 | z+>0 ]>
- => < x:=y; y:=z, [ x+>5 | y+>7 | z+>5 ]>
- => < y:=z, [ x+>7 | y+>7 | z+>5 ]>
- => [ x+>7 | y+>5 | z+>5 ]
This is often called "small-step" semantics. As you can see we, step by step,
derive that
- < z:=x; x:=y; y:=z, [ x+>5 | y+>7 | z+>0 ]> =>^3 [ x+>7 | y+>5 | z+>5 ].
To define these properly we will write down "axioms" like this:
For v1,v2:variables, s:Variables->Values, < v1:=v2, s > => s[v1+> s v2].
To define the idea of "execute, one at a time..." we need a derivation rule
like this
- For S1:Statement,S2:Sequence, s1,s2,s3:Variables->Values,
- if <S1,s1>=>s2
- then <S1;S2, s1>=><S2, s2>.
(meaning:"If S1 turns s1 into s2 in one step then S1;S2 applies S1 giving s2
and then executes S2 in that state. We will see the rest of these rules in
later.
The so called "natural" semantics are natural to write down, not to use! The
make us almost analyze the execution of the program backward from what we know
to be the result.
The notation is
- <S,s>->s'
which mens that if S is started in state s then it terminates with a state of
s'. So if we know that
- < z:=x; x:=y; y:=z, [ x+>5 | y+>7 | z+>0 ]> -> [ x+>7 | y+>5 | z+>5 ]
then the rules (later) show us that the last step was y:=z and
- < z:=x; x:=y; [ x+>5 | y+>7 | z+>0 ]> -> [ x+>7 | y+>7 | z+>5 ]
- and
- < y:=z, [ x+>7 | y+>7 | z+>5 ]> -> [ x+>7 | y+>5 | z+>5 ]
We can repeat the analysis another step... However we present the result of
the analysis as a "Derivation Tree":
- <z:=x, s570> -> s575> <x:=y, s575> -> s775
- -------------------------------------------
- <z:=x; x:=y, s570> -> s775 <y:=z,s775>->s755
- -----------------------------------------------------------
- < z:=x; x:=y; y:=z, s570> -> s755
Note, that you need to abbreviate the state descriptions to make this fit on a
page.
Here each horizontal line is the result of applying one of the rules that
appear as part of the "natural semantics" of sequences:
- For S1:Statement,S2:Sequence, s1,s2,s3:Variables->Values,
- if <S1,s1> -> s2 and <S2,s2> -> s3
- then <S1;S2, s1> -> s3.
. . . . . . . . . ( end of section Operational Semantics) <<Contents | Index>>
In the denotational semantics of this simple language we define a function,
piece by piece that describes the effect of S as a map
- D[[ s ]] : (Variables->Values)->(Variables->Values).
So
- D[[ S ]] s = s'
is true precisely when S terminates and changes state s into state s'.
Typical denotational rules are
D[[ v1 := v2 ]] s ::= s[v1+> s v2]
and
D[[S1; S2]] ::= D[[ S2 ]] o D[[ S1 ]]
where 'o' indicates function composition:
- (f o g)x = f(g(x)).
Notice that these are equations, rather than derivation (if_then) rules. In
our previous example
- D[[z:=x; x:=y; y:=z]] [ x+>5 | y+>7 | z+>0 ]
- =D[[x:=y; y:=z]] (D[[z:=x]] [ x+>5 | y+>7 | z+>0 ])
- = D[[ x:=y; y:=z ]] [ x+>5 | y+>7 | z+>5 ]>
- = D[[ y:=z ]] D[[ x:=y]] [ x+>5 | y+>7 | z+>5 ]>
- = D[[ y:=z]] [ x+>7 | y+>7 | z+>5 ]>
- = [ x+>7 | y+>5 | z+>5 ]
There is a certain elegance about this approach... however it means that when
we model iteration we have to figure out the meaning of iterating functions
before we can write down the equations.
Axiomatic semantic was a very early idea - Floyd's "assigning meanings to
flowcharts" and Hoare's Axioms are seminal work in the theory of programming
and programming languages.
Hoare uses a notation like:
- {Before}Construct{After}
where the Before and After are statements that can be true or false and
contain variables - predicates. For example, we expect the following to be
true:
- { x=5 } y:=x { y=5 and x=5 }
Indeed we have rules like:
For all predicates P1,P2,P3 and statements S1, S2,
- if { P1 } S1 {P2} and {P2} S2 {P3}
- then {P1} S1;S2 {P3}.
And (perhaps) axioms like
For all values u,v,w and variables x,y,z,
- { x=v and z=w and y=u } y:=x {x=v and y=v and z=w}.
Using these we can prove a general result - that the code
- z:=x; x:=y; y:=z
swaps the values of x and y. As a triple this reads:
- {x=n and y=m} z:=x; x:=y; y:=z { x=m and y=n}.
Proof 1
- {x=n and y=m} z:=x {x=n and y=m and z=n} -- Axiom
- {x=n and y=m and z=n} x:=y {x=m and y=m and z=n} -- Axiom
- {x=n and y=m} z:=x; x:=y {x=m and y=m and z=n} -- rule
- {x=m and y=m and z=n} y:=z {x=m and y=n and z=n} -- Axiom
- {x=n and y=m} z:=x; x:=y; y:=z {x=m and y=n and z=n} -- rule
- {x=n and y=m} z:=x; x:=y; y:=z {x=m and y=n} -- simplifying
This is (like denotational semantics) an attempt to develop a calculus for
handling programming. The key idea is of a "Predicate Transformer" - a
function that operates on Predicates to produce predicates. The most
important of these is the "weakest precondition" transformer of a statement
which tells you the least conditions needed to get a particular result. For
example, To be sure that y=n after y:=x we must have that x=n. Further, i
x=n then after y:=x we will have y=n. So
- wp[ y:=x ] (y=n) iff (x=n).
A typical rule is:
- if wp[S1]P2 iff P1 and wp[S2]P3 iff P2
- then wp[S1;S2]P3 iff P1.
(I use 'iff' between equal predicates, so we don't get it confused with '='
between variables and values etc)
Using these you can show that if we want x=5 after z:=x; x:=y; y:=z
then we must have y=5 first, and if y=5 first then x=5 after the sequence.
- wp[y:=z](x=5) iff (x=5) -- axiom
- wp[x:=y](x=5) iff (y=5) -- axiom
- wp[z:=x](y=5) iff (y=5) -- axiom
- wp[x:=y;y:=z](x=5) iff (y=5) -- rule
- wp[z:=x; x:=y;y:=z](x=5) iff (y=5) -- rule
. . . . . . . . . ( end of section Assignment and Sequence) <<Contents | Index>>
Notice that these methods are not really rivals. They are different
techniques for different purposes and (to some extent) apply well to different
languages.
To show this we apply each of them to the same small language (called While)
and explore the ease with which different extensions can be specified.
Further properties of each kind of semantics for While will be explored and
the relationships between the techniques will be developed.
[ while.html ]