## Single-Assignment Form

Consider the two program fragments below and suppose we only care about the values of variables `m`, `n`, `x` and `y` (where the declarations of `m` and `n` are not shown). Under this assumption we regard the two programs as equivalent: they compute identical values for `x` and `y` for any input values `m` and `m`.

1. Immutable-Variable Program

``````val p: Z = m
val q: Z = n
val z: Z = p + q
val y: Z = z - q
val x: Z = z - y
assert(x == n & y == m)
``````
2. Mutable-Variable Program

``````var x: Z = m
var y: Z = n
x = x + y
y = x - y
x = x - y
assert(x == n & y == m)
``````

We have no preference for one program fragment or the other. However, we have seen that proofs of immutable-variable programs appear to be more straightforward because each variable as it appears in the program is associated with a collection of facts that characterise it. In order to deal with mutable-variable programs we have to introduce fresh identifiers for variables as their prior values are overwritten. As a consequence, in proofs mutable-variable programs appear like immutable-variable programs.

We can systematically transform mutable-variable programs into immutable-variable programs, e.g.,

1. Transformed Program
``````val x_At_0: Z = m
val y_At_0: Z = n
val x_At_1: Z = x_At_0 + y_At_0
val y: Z = x_At_1 - y_At_0
val x: Z = x_At_1 - y
assert(x == n & y == m)
``````

Instead of creatively inventing new identifiers (as in program 1), we count from `0` the n-th assignment to each variable. We could also rename the remaining `y` to `y_At_1` and `x` to `x_At_2` but we want to make clear that the final assertion `assert(x == n & y == m)` is unchanged (without stating a side condition `x == x_At_2 & y == y_At_1`). Having transformed program 2 into program 3, where each variable is assigned only once, we can interpret the program as a sequence of equations.

1. Program as Equations
``````x_At_0 == m
y_At_0 == n
x_At_1 == x_At_0 + y_At_0
y == x_At_1 - y_At_0
x == x_At_1 - y
``````

For the program to be correct with respect to the post-condition `x == n & y == m`, the equations must imply the post-conditions.

1. Correctness Condition for the Program
``````  x_At_0 == m
y_At_0 == n
x_At_1 == x_At_0 + y_At_0
y == x_At_1 - y_At_0
x == x_At_1 - y
|-
x == n & y == m
``````

Up to renaming this condition is very close to what we have used in our informal proof in Chapter 1. We only need to replace `v_At_i` (for variable `v` at `i`) by the operator notation `At(v, i)` using the `At`-operator.

1. Correctness Condition for the Program using Operator Notation
``````  At(x,0) == m
At(y,0) == n
At(x,1) == At(x,0) + At(y,0)
y == At(x,1) - At(y,0)
x == At(x,1) - y
|-
x == n & y == m
``````

This condition corresponds to the one shown by Logika when inspecting the facts belonging to the `assert(x == n & y == m)` statement in the last line of program 2. Moving directly from program 2 to condition 6, we observe that programs themselves are facts. This is an interesting insight because we know how to reason about facts, and it is helpful for proving a program correct, for determining test cases and for searching counterexamples in case a program is not correct. An alternative view of programs considers them as transforming facts, tracing them from a pre-condition through a program to the program’s post-condition. This approach is known as symbolic execution.

## A Meta-Notation for Programs

As we have just seen programs themselves are facts. Incidentally, we have used this insight from the beginning when reasoning about programs: we said after an assignment val x = E for some expression E we can use the equality x == E . We have just not been systematic about this. This is the purpose of the current section.

In order to facilitate the discussion we use a notation, that we call meta-notation, distinct from Slang, so that we are always clear about whether we talk about programs in general or about concrete Slang programs. A statement in meta-notation denotes collections of Slang programs by means of meta-variables for which Slang expressions can be substituted. We distinguish meta-variables, say "v" , from other objects by printing them as v . In the table below we introduce the meta-notation for assignment and conditional and give an example for each.

Statement Meta-notation Slang example
Val-Declaration val x = E val m = n + 1
Var-Declaration var x = E var m = n + 1
Assignment x = E m = m + 1
Sequential S1 ; S2 ; ... ; Sn x = x + y; y = x - y
Block { S1 ; S2 ; ... ; Sn } { x = x + y; y = x - y; x = x - y }
Conditional if ( B ) P else Q if (x >= 0) { y = x } else { y = -x }

### Variable conventions

The meta-variables in the table above are intended to be instantiated by specific syntactic Slang objects like variables or expressions. We consistently use a set of meta-variable names as listed in the table below.

Meta-variable Intended instantiation
x , y , z Slang variables
E , F Slang expressions
B , C Slang Boolean expressions
S , T Slang (non-sequential) statements
S1 , S2 , …, Sn n Slang (non-sequential) statements, possible zero
P , Q Slang Blocks

### Remarks

1. Also note, that we usually do not use ; to compose statements sequentially but write the statements in consecutive lines instead. For instance, S1 ; S2 ; ... ; Sn is the same as

S1
S2
Sn
2. Formally, we treat sequential composition ; like a binary associative operator. That is

S1 ; S2 ; S3 ; ... ; Sn   =   S1 ; ( S2 ; ( S3 ; ( ... ; Sn ) ) )
Of course, that parentheses are not part of the syntax. We write them emphasise the that when we analyse sequentials, we only consider pairs S ; T , assuming that S cannot be a sequential.

3. Note, that a block is allowed to empty (for n = 0). An empty block does nothing. In case the else-block of a conditional is empty, we leave the else part of the conditional away. That is, we have the equality

if ( B ) P else { }   =   if ( B ) P .

### Example instantiations from the table

#### Val- and Var-Declaration

Substituting m for x and n + 1 for E in the meta-declarations, both val and var, we obtain the concrete Slang declarations on the right-hand side. Each declaration contains an initial assignment of the newly declared variable. The declared Slang variable, here m , must not occur on the right-hand side of the assignment. It is not known before its declaration.

#### Assignment

Substituting m for x and m + 1 for E in the meta-assignment, we obtain the concrete Slang assignment on the right-hand side. The Slang variable m occurs on both sides of the assignment.

#### Sequential

Substituting x = x + y for S1 and y = x - y for S2 , with n = 2, in the meta-sequential, we obtain the concrete Slang sequential on the right-hand side.

#### Block

Substituting x = x + y for S1 , y = x - y for S2 x = x - y for S3 , with n = 3, in the meta-block, we obtain the concrete Slang block on the right-hand side.

#### Conditional

Substituting x >= 0 for B , { y = x } for S and { y = -x } for T in the meta-conditional, we obtain the concrete Slang conditional on the right-hand side.

## Programs are Facts

• E s subsitution of all x in E by At( x , s[ x ] )

• (a + b)( x ) = a( x ) + b( x )

• (a b | c)( x ) = b( x )     if x c

• (a b | c)( x ) = a( x )     if x c

• x M S if and only if N S ( x ) > 0

• N x = E ( y ) = 1     if x = y ,     0 otherwise

• N val x = E ( y )   =   N x = E ( y )

• N S ; T ( x )   =   N S ( x ) + N T ( x )

• N if ( B ) P else Q   =   max( N S ( x ), N T ( x ) )

• F { } ( x ) = 0

• N { S1 ; S2 ; ... ; Sn } ( x )   =   N S1 ; S2 ; ... ; Sn ( x )     provided n > 0

• eq(a, S , T ) ) = V x1 (a + N S ) == V x1 (a + N T ) & & V xk (a + N S ) == V xk (a + N T )     for all those j between 1 and k with N S ( xj ) < N T ( xj )

• V x (a)   =   At( x , a[ x ] )

• F x = E (a, s)   =   V x (a) == E s

• F val x = E (a, s)   =   F x = E (a, s)

• F var x = E (a, s)   =   F x = E (a, s)

• F S ; T (a, s)   =   F S (a, s) & F T (a + N S , s a | M S )

• F { } (a, s)   =   true

• F { S1 ; S2 ; ... ; Sn } (a, s)   =   F S1 ; S2 ; ... ; Sn (a, s)     provided n > 0

• F if ( B ) P else Q (a, s)   =   ( B => F P (a, s) & eq(a, P , Q ) ) & ( !B => F Q (a, s) & eq(a, Q , P ) )