# Using Relational Semantics

We next show how to use relational semantics to prove properties of specific programs, by checking relation subset.

We also apply relational semantics to prove two normal-form theorems about programs.

## Proving Program Properties

A general approach:

• compute semantics of a program as a mathematical object (e.g. relation)
• prove that the relation satisfies the desired property

### Example

Consider the code

r = 0;
i = y;
while (i > 0) (
r = r + x;
i = i - 1
)

We represent it as

r = 0;
i = y;
loop (
assume (i > 0);
r = r + x;
i = i - 1
);
assume (i <= 0);

We compute the meaning of

assume (i > 0);
r = r + x;
i = i - 1

as the relation whose formula is

We then wish to compute the transitive closure .

We claim that for every relation is given by formula

We can prove this claim by induction. The union of these relations is then given by

From there we can derive the meaning of

r = 0;
i = y;
loop (
assume (i > 0);
r = r + x;
i = i - 1
)

as

which when composed with assume() = assume() gives

which is equivalent to

This is the semantics of the above code.

## Relations as Specifications

Nondeterministic programs can be used to specify other programs

If is relation representing program and relation representing specification, we say that program meets specification iff

Example:

This allows us to prove that programs satisfy their contracts, expressed using preconditions and postconditions:

void f()
requires x > 0
ensures x > 0
{
x = x + 1;
}

What is the relation for contract with

• precondition
• postcondition

The correctness condition:

reduces to:

## While Theorem

Definition: Control-Flow Graph (CFG) is graph where

• is set of CFG nodes, representing program points
• set of CFG edges (represent jumps)
• gives a CFG statement for each edge
• statements
• conditions

Note: there are alternative representations

• putting statements on nodes instead of edges
• labelling outgoing edges

Transforming an example program to control flow graph.

We can describe the meaning of the program by writing one loop that traverses the control-flow graph.

Every program has a control-flow graph, so every program can be written using one loop.

The body of this loop is a relation, which we call transition relation. It can be described by the formula that has a particular form: disjunction of conjunctions, where each conjunction describes changes happening in one edge of the control-flow graph.

## Normal Form for Loop-Free Programs

Example:

(if (x < 0) x=x+1 else x=x);
(if (y < 0) y=y+x else y=y);

Without loops, after expressing conditionals using [] we obtain

c ::=  x=T | assume(F) |  c [] c  |  c ; c

Laws:

Using these laws, we can reduce each program in the syntax above into the following normal form:

Each is of form for some , where each is assignment or assume. Each corresponds to one of the finitely paths from beginning to end of the acyclic control-flow graph for loop-free program.

Length of normal form with sequences of if-then-else can be exponential in the size of the program.

In general, we would like to postpone explicit enumeration of these paths as long as possible.