What's the difference between: operational, denotational and axiomatic semantics?

Question

Recap of the terms from the dictionary:

• semantics: the study of meaning in a language (words, phrases, etc) and of language constructs in programming languages (basically any syntactically valid part of a program that generates an instruction or a sequence of instructions that perform a specific task when executed by the CPU)
• operational: related to the activities involved in doing or producing something
• denotational: the main meaning of a word
• axiomatic: obviously true and therefore not needing to be proved

Wikipedia's main article about: semantics.

Operational semantics:

This says that the meaning of a language construct is specified by the computation it induces. It is of interest how the effect of a computation is produced. My understanding of this is that this basically describes the meaning of all the operations involved in a program (from the most basic to the most complex).

Examples:

arithmetic operations: 1 + 1, 10 ** 2, 19 // 3 etc. In this case it analyzes the meaning of the steps involved in producing a result given n operands and n operators. This can be further boiled down to what each operand means (so in my examples each number is defined in the domain of natural numbers [1, 2, ..., n], etc.

assignment operations: x = 5, y = 5 ** 2, z = 10 ** 2 // 3 * (99 + 1024) etc. In this case it involves an evaluation of the value of the mathematical expression on the right and assigning it to the identifier on the left.

augmented assignment operations: x += y, z *= t etc. In this case it involves an evaluation of each identifier once, and performing an arithmetic operation first, followed by an assignment operation last. etc.

Denotational semantics:

This says that meanings are modelled by mathematical objects that represent the effect of executing the constructs. It is of interest only the effect of a computation, not how it is produced. My understanding of this is basically that it's related to mathematical functions, which take something as an input, do some computation which you don't care about and produce a result, which you care about. Since denotational means the main meaning, I take this as: the name of your functions/methods/identifiers should constrain the possible interpretations of what they do, ideally to be exact.

Examples:

sort(iterable): should pretty much do what it says, take an unordered iterable as its input and return it ordered (you don't care how it does that under the hood)

min(iterable): should take an array return the smallest value (you don't care how it does it)

max(iterable): should take an array return the largest value (you don't care how it does it) etc.

Axiomatic semantics:

Some properties of the effect of executing the constructs are expressed as assertions. Some aspects of the executions may be ignored. My understanding of this is that it's related to boolean algebra and logic.

Examples:

expr1 and expr2: if expr1 is False then the entire boolean expression is False and it short-circuits and expr2 is not evaluated

Or even compound statements:

if expr1:
elif expr2:
elif expr3:
else:

The effect is the result of executing the above construct and you assert its value based on whichever boolean expression yield true, the rest of them being ignored.

Question:

Are my examples for each category of semantics accurate and if not can one please provide some simple (not formal as Wikipedia does it with mathematical formulas, etc) examples of each semantic category? Examples that would match what we encounter in normal, day to day computer programs.

The gist of it is that semantic ties an identifier (word, symbol, sign) to its real meaning. The way it does this can be further boiled down to:

Operational semantics ties any type of operation (arithmetic, assignment, etc.) to the computation involved.

Denotational semantics ties identifiers to their meaning (so this is basically the most common one in programming). It's when you define a function it should do what it says. So for instance if you define a function dat says add_numbers(x, y) it should add x to y and not multiply them.

Axiomatic semantics ties the outcome of constructs to assertions. Basically boolean algebra (short-circuits in logical expressions, code branching (if-elif-else, switch-cases, etc).

Answer 1

I think your examples show you do somehow understand the basic points of the several styles of semantics. Still, note that the whole point of having a semantics of a programming language is to have a formal, mathematically rigorous description of the program behavior. That inherently involves math and several formulae -- one can't really do without math. Math is used as the foundation of every science, and computer science is no exception to this fact.

You are correct when you say that the denotational semantics for a program is, very roughly, a function from its input to its output. E.g. "this program computes the factorial function on naturals". Things start being more complex here when we want to model that the program might not terminate, or when the result is not a simple number but rather a record (an object, if you prefer) containing functions, which in turn might not terminate (or return another record which ...). The mathematical models which arise there become less and less trivial as soon as you allow for more complex data types (e.g. polymorphic functions).

Operational semantics of imperative programs roughly relates the initial variables state to the final one. E.g. "if we start the program with $x=3,y=4$ we end up with $x=7,y=2$". If the semantics is in "small step" style, we further get to see all the intermediate values of variables, as if we were running a debugger and stepping through each program line, so to speak. Such "small step" semantics allows to count, say, the number of multiplications performed by the program, which can not be seen in its denotation alone (however, note that, if we consider that count to be a kind of "observable output", we could define another denotational semantics returning that count as well -- the semantics styles are rather flexible).

Axiomatic semantics instead roughly works with set of states instead of single ones. It can express statements like "if we start the program with variables having any value satisfying $x>y>5$ we end up with $x<100,y=x^2$". Note that we do not know the exact value of each variable here, but only a property that variables satisfy, expressed using logic.

That being said, if you want to achieve a solid understanding, you really have to read about the technical details: all the mathematical definitions and basic theorems. This is not hard, but is also not trivial either -- typically, a single university course can cover the basics of each style.