Table of Contents
While programs constitute a set of deterministic programs. A while program is a string of symbols, they represent the core of ALGOL-like languages. An abstract syntax is given for the formulation of while programs:
where form the set of variables and B denotes a Boolean and E stands for an arithmetical expression, respectively. We write for the set of while programs.
Unless otherwise stated by Boolean expressions we mean the set of formal arithmetic expressions built from natural numbers, variables and usual number theoretic functions and relations like summation, subtraction, multiplication, division, equality, less than or equals and so on.
For the sake of clarity, we give some elementary definitions of these notions. For the time being, we restrict ourselves to basic arithmetic operations. We assume a fixed domain to be given, it is either the set of natural numbers or the set of integers. Unless otherwise stated let denote the natural numbers. Let capital letters X, Y , etc. denote variables, and let n, stand for elements of . Then
are arithmetical expressions. The set of arithmetical expressions is denoted by . If represents the natural numbers, then subtraction is understood as follows:
Otherwise it is the usual subtraction of integers. In the sequel, by an abuse of notation, we use instead of . In the definition below let , be arithmetical expressions. Then
are Boolean expressions. The set of Boolean expressions is denoted by . In order to facilitate writing expressions we use usual conventions for the order of evaluation of operators: multiplication is evaluated before addition and subtraction etc. We also introduce convenient abbreviations, like
If possible, we omit parentheses in Boolean expressions, stipulating that conjunction and disjunction binds stronger than implication, which is stronger than equivalence. Negation is stronger than any of the two argument logical operations.
With this in hand we can turn to the informal explanations of the elements of a program. The meaning of is self explanatory: it always terminates and leaves everything as was before its execution. We can define the abbreviation then
The command , where X is a variable and E is an arithmetical expression, is called an assignment. The meaning of the conditional statement is again self explanatory, whereas the while statement, or loop, acts as follows. It evaluates the Boolean expression following the while, which is the head of the loop, and, if it evaluates to true, the execution continues with the body of the loop. After the body of the loop has terminated, the head of the loop is evaluated again. The while statement terminates when the head of the loop evaluates to false. Of course, for proving statements about programs this informal explanation is not enough. That’s why we turn to a more rigorous description of the behaviour of programs. We need the notion of a state:
In effect, the while program is a function manipulating states. We start from the initial state, and to every execution of a component of the program a state is attached. When the program terminates, we obtain the result of the execution by reading the values assigned to the variables of the program by the final state, which is the state attached to the program at the time of termination. We can make precise these notions as follows. We introduce a more general form of a transition system than needed for our present purposes, since we will be able to make use of this definition even in the subsequent parts of the course material.
We define the operational semantics of a program as a transition system. The definition is compositional: knowing the transitions for the subprograms of the program we can determine the behaviour of the program itself. Beforehand, we have to define the meaning of the arithmetical and Boolean expressions, respectively. We assume an interpretation is given, where is a mapping assigning concrete values to constants and functions and predicate symbols appearing in arithmetical expressions. Then the truth values of Boolean expressions are obtained in the usual way. As an abuse of notation, we denote the values assigned by to the constant c, function symbol f by and instead of and , respectively. If B is true in the model with respect to an interpretation s, we write , or . If the states are not interesting for our treatment, we may omit them. Moreover, for a Boolean expression B, let . Thus identifies a subset of .
In the definition below let be states, B be a Boolean expression and be programs, respectively. The elements of the transition system belonging to a program C are elements of , where are the subprograms of C. We denote by . The transitions are defined as follows:
starting from s is a computation if it is infinite or cannot be extended any further. A computation is terminating if its last configuration is an element of . C can diverge from s if there is a diverging computation starting with .
Example 7. Let C be the program of Example 2. Let , and otherwise. For the moment, let us denote s by a triple representing the values assigned to X, Y and Z, respectively. Then
where is C with the first assignment omitted, and is the body of the while loop in C.
An alternative approach to the operational semantics is to construct a set of pairs as the operational semantics of a program in a direct way (cf. ). As before, let . Then , where is the set of subsets of A, is defined as follows. In the definition below, let , where s is a state and E is an arithmetical expression, denote the state which is identical to s except for the value at X, for which .
As an example let us consider the following simple program.
Intuitively, the program terminates for every , and when it terminates the value of Y equals the starting value of X. Let C denote the whole program, be the while loop and let stand for the body of the loop. Then:
From the set of pairs we can extract a computation sequence for any given state s. For example, let , assume all the other values of s are zero. In the example below we denote s by its X and Y values. Then
is a computation for C with .
Without proof we state the equivalence of the two approaches. In the theorem below, let denote the reflexive and transitive closure of .