CMP 332
SURVEY OF PROGRAMMING LANGUAGES
LANGUAGE DESCRIPTION (SEMANTIC STRUCTURE)
LECTURE FIVE
Delivered By: Dr. T. A. Olowookere
Lesson objectives
By the end of this lesson, students should be able to:
Understand Formal and Informal semantics
Overview of formal semantics
Formal semantics styles
Denotation semantics
Axiomatic semantics
Operational semantics
Semantics Description
The semantics of a language describe the meaning of a given
statement.
"Semantics" deals with the meaning of the ideas themselves.
Semantics: the meaning of the expressions, statements, and
program units, that is, the study of meaning of languages.
It describes the meaning of language constructs (refering to the
relationship between signifiers like words, signs, symbols and
what they stand for in reality)
Informal Semantics
• A programming language can have both formal and informal semantics
the informal semantics serves as a "plain-text" explanation of the formal
semantics, and the formal semantics would be the place to look if you're not
sure what the informal explanation really means.
1-4
Formal semantics
Formal semantics is the mathematical theories for ascribing meanings to
computer languages.
Formal semantics for programming languages can also be described as the
study of formalization of the practice of computer programming.
A computer language consists of a (formal) syntax – describing the actual
structure of programs and the semantics – which describes the meaning of
programs. Many tools exist for programming languages (compilers,
interpreters, verification tools, ... ), the basis on which these tools can
cooperate is the formal semantics of the language.
Formal semantics, for instance, helps to write compilers, it gives better
understanding to what a program is doing and to prove, e.g., that the following
if statement
if 1 = 1 then S1 else S2
has the same effect as S1 alone.
1-5
Difference between formal and informal semantic
• formal semantic are dependent on syntax rules.
• Informal semantic can use the common context
shared as a basis to support meaning.
1-6
Advantages of formal semantics
A formal semantics ...
is simpler than an implementation, more precise than intuition
can answer: is this implementation correct?
supports the definition of analyses and transformations
prove properties about the language
prove properties about programs written in the language
promotes better language design
better understand impact of design decisions
apply semantic insights to improve the language design (e.g
compositionality)
1-7
Styles of formal semantics
There are many styles/approaches to formal semantics;
these belong to three major classes:
Operational.
Meanings for programphrases defined in terms of the steps of
computation they can take during program execution. (related to
the activities involved in doing or producing something)
Axiomatic.
Meanings for program phrases defined indirectly via the axioms
and rules of some logic of program properties.
Denotational.
Concerned with giving mathematical models of programming
languages. Meanings for program phrases defined abstractly as
elements of some suitable mathematical structure.
1-8
In computer science, denotational semantics (initially known as
mathematical semantics or Scott–Strachey semantics) is an approach of
formalizing the meanings of programming languages by constructing
mathematical objects (called denotations) that describe the meanings of
expressions from the languages.
Broadly speaking, denotational semantics is concerned with finding
mathematical objects called domains that represent what programs do.
For example, programs (or program phrases) might be represented by partial
functions or by games between the environment and the system.
1-9
Denotational Semantics
This says that meanings are modelled by mathematical objects that
represent the effect of executing the constructs.
It is of interest to only the effect of a computation, not how it is
produced.
This describes basically, 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, the name of your
function should constrain the possible interpretations of what it
does, ideally to be exact.
Denotational Semantics
Examples:
sort(iterable): should pretty much do what it says, take an unordered
iterable as its input and return it ordered.
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)
abs(x): return the absolute value of a number
etc.
Denotational Semantics
The following properties of a denotational semantics are often of interest.
Syntax independence: The denotations of programs should not involve the syntax of the
source language.
Soundness: All observably distinct programs have distinct denotations.
Full abstraction: Two programs have the same denotations precisely when they are
observationally equivalent. For semantics in the traditional style, full abstraction may be
understood roughly as the requirement that "operational equivalence coincides with
denotational equality".
Additional desirable properties we may wish to hold between operational and denotational
semantics are:
Constructivism: Constructivism is concerned with whether domain elements can be shown to
exist by constructive methods.
Independence of denotational and operational semantics: The denotational semantics should
be formalized using mathematical structures that are independent of the operational
semantics of a programming language; However, the underlying concepts can be closely
related.
Full completeness or definability: Every morphism of the semantic model should be the
denotation of a program.
Summary
Denotational semantic definition has five parts:
• Semantic equations
• Syntactic categories
• Semantic functions
• Backus normal form (BNF) defining the structure of the syntactic categories
• Value domains
Denotational semantics have been developed for modern languages which have features like
exceptions and concurrency. One of the important features of denotational semantics is that
semantics should be compositional, meaning denotation of a programming phrase can be
constructed from the denotations of its sub-phrases.
There are some distinct advantages associated with denotational semantics. It is the easiest
mechanism for describing the meaning of smaller programs compared to other alternatives.
Denotational semantics is capable of explaining state in programs. However, denotational
semantics tend to be very complex for describing advanced features like goto statements and
recursions.
1-13
Evaluation of Denotational Semantics
• Can be used to prove the correctness of
programs
• Provides a rigorous way to think about
programs
• Can be an aid to language design
• Has been used in compiler generation
systems
• Because of its complexity, it is of little use to
language users
1-14
Axiomatic Semantics
• Axiomatic semantics define the meaning of a command in a
program by describing its effect on assertions about the program
state.
• Axiomatic semantic is based on formal logic (predicate
calculus)
• Original purpose: it is formally use in program verification
• Axioms or inference rules are defined for each statement type in
the language (to allow transformations of logic expressions into
more formal logic expressions)
• The logic expressions are called assertions. The assertions are logical
statements—predicates with variables, where the variables define
the state of the program.
1-15
Axiomatic Semantics
Axiomatic semantics describes the meaning of programs in terms of properties
(axioms) about them.
Some properties of the effect of executing the constructs are expressed as assertions.
Some aspects of the executions may be ignored. It is related to Boolean algebra and
logic.
Every language construct is described in terms of a statement (in logic) about what
the construct accomplishes when it executes.
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.
Axiomatic Semantics (continued)
• An assertion before a statement (a precondition )
states the relationships and constraints among
variables that are true at that point in execution
• An assertion following a statement is a
post condition
• A weakest precondition is the least restrictive
precondition that will guarantee the post
condition
1-17
Examples
• {x≤10} while (x<=10) do x:=x+1 {x=11}
• [x≤10] while (x<=10) do x:=x+1 [ ? ]
1-18
Operational Semantics
Operational semantics describes the meaning of programs in terms
of the execution steps taken by an abstract machine.
Properties of Operational semantics
relatively simple
not compositional (rule for while)
Good for
–describing language implementation
– reasoning about properties of the language• eg. determinism
– reasoning about of tools that manipulate programs• eg. compilers,
type
checkers, etc
Not good for automatic reasoning about programs
1-19
Operational Semantics
This depicts that the meaning of a language construct is specified
by the computation it induces.
What is of interest in axiomatic semantics is how the effect of a
computation is produced.
Operational semantics describes the meaning of programs in terms of
the execution steps taken by an abstract machine.
It basically describes the meaning of all the operations involved in
a program (from the most basic to the most complex).
Operational Semantics (continued)
Operational semantics is a category of formal programming language
semantics in which certain desired properties of a program, such as
correctness, safety or security, are verified by constructing proofs from
logical statements about its execution and procedures, rather than by
attaching mathematical meanings to its terms (denotational semantics).
Operational semantics are classified into two categories:
• structural operational semantics (or small-step semantics) formally
describe how the individual steps of a computation take place in a
computer-based system.
• By opposition natural semantics (or big-step semantics) describe how
the overall results of the executions are obtained.
1-21
Operational Semantics
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.
Denotation Semantics vs Operational Semantics
• In operational semantics, the state changes are
defined by coded algorithms
• In denotational semantics, the state changes
are defined by rigorous mathematical
functions
1-23
