Examples of Three Semantic Specifications:
Operational semantics is based upon the imperative model of the language,
describing the semantics of a language by mapping programs in that
language into equivalent programs implemented on an abstract machine.
Denotational semantics use functional model of languages to map
programs in that language into equivalent functions.
Axiomatic semantics is based on the logic model of programming languages
describing the action of a program by determining logical assertions that
hold before and after its execution.
For all examples, we use the following Calculator Grammar
Cal -> Exp =
Exp -> val | val opr Exp // Right-associativity
val -> sign int | int | sign int . dec | int . dec
int -> d | int d
dec -> d | d dec
d -> 0 | 1 | 2 |3 | 4 | 5 | 6 | 7 | 8 | 9
sign -> + | -
opr -> + | - | * | /
1. Operational
A. Use a simple stack machine as our abstract machine with
the following six instructions:
push value: push the given value on the stack
pop: pop the top value
add: add top two values, replacing them by their sum
sub: substract top two values, replacing likewise.
mult: multiply top two values, replacing likewise.
div: divide the top two values, replacing likewise.
B. Stack machine codes for the Operational Semantic.
For each syntax production rule, these codes need to be defined.
For example, for the rule: int -> int d
the following stack machine code may be defined:
Code to be generated by RHS int, followed by
push 10
mult
Code to be generated by RHS d
add
Complete Operational Semantics:
Cal -> Exp = | #Exp# // code to be generated
| // by RHS Exp
| pop
Exp -> val | #val#
Exp -> val opr Exp | #Exp#
| #val#
| #opr#
Val -> sign int | #int#
| #sign#
Val -> int | #int#
Val -> sign int . dec | #int#
| #dec#
| add
| #sign#
Val -> int . dec | #int#
| #dec#
| add
int -> d | #d#
int -> int d | #int#
| push 10
| mult
| #d#
| add
dec -> d | push 10
| #d#
| div
dec -> d dec | push 10
| #dec#
| div
| push 10
| #d#
| div
| add
d -> 0 | push 0
d -> 1 | push 1
d -> 2 | push 2
// And, similarly, for each of other seven digits
sign -> + | No op.
sign -> - | push -1
| mult
opr -> + | add
opr -> - | sub
opr -> * | Mult
opr -> / | div
Example: 1.5*-40=
The following codes will be generated:
push 4
push 10
mult
push 0 End for int(40)
add
push -1
mult End for val(-40) and for Exp(-40)
push 1
push 10
push 5
div
add
mult
pop
2. Denotational Semantics:
A. Key Ideas:
a. For each nonterminal of the Grammar,
we define a function that maps a syntactic structure
(in the Syntactic Domain) into a value in the Semantic Domain.
b. In defining such a function, we consider all production rules
of the corresponding nonterminal.
c. When the final (ultimate) function for the starting nonterminal
is applied to a source program, the function must yield
the expected output(s) of this program.
For example, for our example Calculator grammar, if Cal() is the function
for the starting nonterminal, then
Cal("100-20+30=") must yield 50.
B. Example production rule.
Let us consider the following production rule and its function:
int -> int d
And assume that Int() is the function for this nonterminal, int.
Int ("int" "d") = 10*Int("int") + D("d")
where D() is the function for the nonterminal d
For the other production rule, int -> d, we will have
Int ("d") = D ("d")
C. Complete Denotational Semantic specification.
Cal(expression) = Exp(expression)
Exp(value) = V(value)
Exp(value '+' expression) = V(value) + Exp(expression)
Exp(value '-' expression) = V(value) - Exp(expression)
Exp(value '*' expression) = V(value) * Exp(expression)
Exp(value '/' expression) = V(value) / Exp(expression)
V('+' int) = Int(int)
V('-' int) = - Int(int)
V(int) = Int(int)
V('+' int '.' dec) = Int(int) + Dec(dec)
V('-' int '.' dec) = - Int(int) - Dec(dec)
V(int '.' dec) = Int(int) + Dec(dec)
Int(d) = D(d)
Int(int d ) = 10*Int(int) + D(d)
Dec(d) = 0.1*D(d)
Dec(d dec) = 0.1(Dec(dec)+D(d))
D('0') = 0
D('1') = 1
...
D('9') = 9
D. Derivation of Denotational functions for: 1.56*-40
Cal("1.56*-40") =
Exp("1.56*-40") =
V("1.56") * Exp("-40")
(Int("1") + Dec("56")) * Exp("-40")
(D("1") + Dec("56")) * Exp("-40")
(1 + Dec("56")) * Exp("-40")
(1 + 0.1(Dec("6")+D("5"))) * Exp("-40")
(1 + 0.1(0.1(D("6"))+D("5"))) * Exp("-40")
(1 + 0.1(0.1(6)+D("5"))) * Exp("-40")
(1 + 0.1(0.6+D("5"))) * Exp("-40")
(1 + 0.1(0.6+5)) * Exp("-40")
(1.56) * Exp("-40")
1.56 * V("-40")
1.56 * (-Int("40"))
1.56 * (-(10*Int("4")+D("0")))
1.56 * (-(10*D("4")+D("0")))
1.56 * (-(10*4+0))
1.56 * (-40)
-62.4
3. Axiomatic Semantics
A. Key ideas
a. For each production rule of the grammar, we define
the effect of executing a structure defined by the rule
in terms of the precondition and the postcondition.
b. The precondition is a logical assertion to be held true
before a structure is executed and the postcondition
is a logical assertion to be true after its execution.
c. The postcondition of the starting nonterminal represents
what the outputs of a program should represent.
d. Useful in program correctness proof.
B. Some notations.
a. $S$->v : An assertion that a structure S evaluates to a
value v
b. output(v) : A value v being output
c. apply(opr, v1, v2)
: The operator 'opr' is applied to the two operands
v1 and v2.
d. Exp(l) : The nonterminal Exp on the LHS of the rule.
e. Exp(r) : The nonterminal Exp on the RHS of the rule.
C. Complete specification of our Calculator grammar:
Production rule Precondition Postcondition
--------------- ------------ -------------
Cal -> Exp = $Exp$-> v output(v)
Exp -> val $val$-> v $Exp$-> v
Exp -> val opr Exp $val$-> v1 and $Exp$->
$Exp(r)$-> v2 apply(opr,v1,v2)
val -> sign int $sign$->v1 and $val$->v1*v2
$int$->v2
val -> int $int$->v $val$->v
val -> int . dec $int$->v1 and $val$->v1+v2
$dec$->v2
val -> sign int . dec
$sign$->v1 and $int$->v2
$dec$->v3 $val$->v1*(v2+v3)
int -> d $d$->v $int$->v
int -> int d $int(r)$->v1 and $int(l)$->10*v1+v2
$d$->v2
dec -> d $d$->v $dec$->v/10
dec -> d dec $d$->v1 and $dec(l)$->(v1+v2)/10)
$dec(r)$->v2
d -> 0 No precondition $d$->0
d -> 1 No precondition $d$->1
...
d -> 9 No precondition $d$->9
sign -> + No precondition $sign$->1
sign -> - No precondition $sign$->-1
D. Another Example
Specifying precodition and postcondition for other statements
(including assignment statement that is used in the above example)
a. Assignment statement: X->E
{P}S{Q} //Notation for a statement S with precondition P
and postcondition Q
As a theorem, it says that if P is true before
the execution of the statement and if the statement
is actually executed, then Q is true after the
execution.
That is, (P and execution of S) -> Q
It is more convenient to compute the precondition from
the desired postcondition as generally we will have a certain
expected results (and conditions for the outcomes of executing
statements and the whole program) and also some assignment
statements are not easily invertible.
For example, X=X*X+Y*Y+Z*Z
It is not straightforward or often even impossible to express
the old value of X and of Y and of Z, respectively,
in terms of the new value of X, which we would need if
we compute the postcondition from the precondition.
For assignment statement, we can compute the (weakest) precondition
as an axiom (as an immediately obtainable logical expression) in
P = Q(X->E) where Q(X->E) is the assertion to be obtained
by replacing every occurrence of X by E.
For example, {P} X=X+Y {X>Y+Z}
In this case, P=((X+Y)>Y+Z)
=X>Z
b. Selection statement: If B then S1 else S2.
There cannot be an axiom as the precondition depends on
the type of two statement S1 and S2.
We can specify a rule (of inference) to specify how the
precondition can be computed.
In order to have: {P} (If B then S1 else S2) {Q}
it is necessary that {B and P} S1 {Q} and
{not(B) and P} S2 {Q}
For example, consider the following if statement:
if (X>Y) then X=X-1 else Y=Y-2
Suppose that postcondition is X+Y>Z
{P1} X=X-1 {X+Y>Z} where P1 is the weakest precondition
for the 'then' part
P1 = (X+Y>Z+1)
{P2} Y=Y-2 {X+Y>Z}
from which, we get P2 = (X+Y>Z+2)
Since P2 implies P1, we can take P2 for P.
That is, {X+Y>Z+2} if (X>Y) then X=X-1 else Y=Y-2 {X+Y>Z}
c. Logical Pretest Loops: while B do S end
This is most difficult type of a statement as a loop is a
sequence of unknown number of statements comprising the loop body.
The key idea is to figure out an assertion, called "Loop Invariant"
that is going to hold both before and after each execution of
the loop body, S.
This is because if "{I and B} S {I}" where I is the loop invariant
then "{I} while B do S end {I and not(B)}.
And, any P that implies I and any Q implied by (I and not(B))
can be the wanted precondition and postcondition.
To be useful, the loop invariant must satisfy the following:
a. P -> I //(if P is true then I is true)
b. {I} B {I} // Evaluation of B does not change I
c. {I and B} S {I} //I is true before and after each
//iteration of the loop body
d. (I and not(B)) -> Q
e. The loop terminates
Actually finding a suitable/appropriate invariant is not
easy. It is much similar to the problem of finding the inductive
hypothsis in mathematical induction.
We will just check for some initial numbers of loop
iterations including zero iteration to see if any pattern
develops.
Example: XX=X
YY=Y
while (YY<>0) do // repeat as long as YY not zero
{ T=XX
XX=YY
YY=(T%YY) // Remainder
}
In the above example, if the postcondition is: XX=GCD(X,Y)
then I can be GCD(X,Y)=GCD(XX,YY)?
So, we can set P to I.
That is,
{GCD(X,Y)=GCD(XX,YY)} the loop statement {XX=GCD(X,Y)}
4. Comparison of three specifications.
a. Operational
Most detailed
Close to compiler/interpreter, and useful for language
implementation tool as long as the descriptions are kept
simple and informal.
Depends on algorithms and not mathematics.
The statements of one language are described in terms of
statements of a lower-level programming language, which can
lead to circularities
b. Denotational
Most rigorous widely known and practical method.
Solidly based on recursive function theory
as functions are used in mapping a syntactic structure
onto instances of well-defined mathematical objects and
the resulting mathematically objects together represent
the meaning of a program.
A good language design aid (a construct for which the
specification is complex and difficult may suggest
that it is not that viable)
Because of the complexity, a little use to language users.
c. Axiomatic
Defining an axiom or a rule of inference for each type
of a programming language has proven to be a difficult task.
Powerful tool for research into program correctness proofs.
Provides an excellent framework for reasoning about programs.
Its usefulness in describing the meaning of a programming
language to either language users or compiler writers is
limited.