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.,

3. 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.

4. 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.

5. 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.

6. 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 .

   We return to this later.

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 ) )

Test Case Generation

Counterexample Generation

Proof

Programs are Fact Transformers

Symbolic Execution

Strongest Postcondition and Weakest Precondition

Synthesis

Dynamic and Static Perspectives

Questions, Perspectives and Answers

Often it is important to look at a problem from the right angle to be able to ask questions whose answers help solving the problem.

Understanding

Having multiple perspectives that provide consistent views on the same program greatly aids in analysing that program.