Programming semantics: introduction

Got it! This site uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website.nbsp; Note: This appears on each machine/browser from which this site is accessed.

The syntax of a language has to do with the punctuation and grammar rules of the language.

The semantics of a language has to do with the underlying meaning of the language.

syntax (what it says)
semantics (what it means)

There are three main ways to reason about programming semantics.

operational semantics
axiomatic semantics
denotational semantics

The operational semantics of a programming language provide a way to understand and reason about programs using an underlying machine architecture that describes how the programs operate.

The axiomatic semantics of a programming language provides rules, called axioms, for understanding and reasoning about program correctness.

The denotational semantics of a programming language uses mathematics for understanding and reasoning about program correctness.

Denotational semantics is very complicated and is usually used to prove that the rules for an axiomatic semantics are well-founded and correct.

The syntax of a language is the rules for grammar and punctuation.

Consider the assignment statement in imperative programming languages.

C, C#, Java, etc.: variable = expression ;
Python, Lua: variable = expression
Pascal: variable := expression ;
Basic: Let variable = expression

The semantics of a language is concerned with the meaning of the syntax.

C, C#, Java, etc.: variable = expression ;
Python, Lua: variable = expression

The semantics of the assignment statement in imperative programming languages is as follows.

1. Evaluate the expression on the RHS (Right Hand Side) to a value.
2. Destructively place the value in the variable location specified by the variable on the LHS (Left Hand Side) .

This description is an operational semantics.

Operational semantics is concerned with "how it works".

The problem with operational semantics is that it does not provide a convenient way to reason about large programs composed of more than a few statements.

Do the following statements swap the values of variables x and y? Provide a clear answer?

x = y; y = x;

What is your reasoning? Be specific.

What do the following assignment statements do? That is, what is their effect.

x = y - x; y = y - x; x = x + y;

Explain how you arrived at your conclusion.

Assignment statements, in conjunction with the destructive update, cause major problems in writing correct programs.

Functional programming languages make it easier to write correct programs, but imperative (i.e., assignment-based) languages are often more machine efficient.

In using imperative programming languages, techniques such as axiomatic semantics are often useful in proving program correctness properties.

There are three main ways of reasoning about the semantics of a programming languages and of a program.

Operational - machine based
Axiomatic - rule based
Denotational - math based

Usually, denotational semantics is used to prove the correctness and soundness of rules for axiomatic semantics (i.e., proof rules).