In learning a programming language, it’s not enough that we study only the syntax. We have to know what is underlying meaning of the syntax we’re typing – i.e. what your code actually does.
There are basically three ways to formally define a language through its’ semantics: (a) operational – through algorithm, (b) denotational – through mathematical equations and objects , and (c) axiomatic – through logic to prove the correctness of a program.
Operational Semantics
The purpose of this approach is to describe how a computation is performed step-by-step. For instance, in a Java program, the Java Virtual Machine (JVM) does that for us. This type of semantics is very familiar especially those who read how-to books of a programming language since we can understand the operational semantics of a program using pseudocode.
For instance, in Java:
if (condition) {
doSomething1();
} else {
doSomething2();
}
Its’ operational sematics:
if condition = true goto doSomething1()
else goto doSomething2()
Given that condition is a boolean that can have a value of either true or false.
Denotational Semantics
Denotational Semantics is an approach that describes the meaning (denotation) of a program using mathematical objects. Usually, they are functions of some sort.
Let Σ be the set of all program states in a programming language. A boolean expression Bexp can be described in a denotation as:
B: Bexp → (Σ → {true, false})
A variable that has been assigned as a boolean can only have values true or false, and the whole assignment expression means that it can only be true or false. The syntactic equivalent of this expression depends on the programming language (i.e. in Java it is boolean b = true; or boolean b = false;)
Axiomatic Semantics
Axiomatic Semantics asserts the relation will always be true for an input and output interface in a program, each time the program is executed.
The semantic formula is of the form
{P} S {Q}
where P is a a pre-condition, S is the command or the control structure, and Q is the post-condition. It is read as the statement S is correct with respect to pre-condition P and post-condition Q. If P is satisfied and S halts, S terminates in a state where assertion Q is satisfied.
For instance, we would like to prove that:
{x = X ∧ y = Y ∧ z = Z} min(X, Y, Z) {min = min(X, Y, Z)}
So,
{x = X ∧ y = Y ∧ z = Z}
min = x; {min = X}
if (min > y) {x = X ∧ y = Y ∧ z = Z ∧ X > Y}
min = y;
{min = Y}
if (min > z) {x = X ∧ y = Y ∧ z = Z ∧ (X > Z ∨ Y > Z)}
min = z;
{min = Z}
{min = min(X, Y, Z)}
