Testing From Implementations
SingleAssignment 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
.

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

MutableVariable 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 immutablevariable 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 mutablevariable programs we have to introduce fresh identifiers for variables as their prior values are overwritten. As a consequence, in proofs mutablevariable programs appear like immutablevariable programs.
We can systematically transform mutablevariable programs into immutablevariable programs, e.g.,
 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 nth 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.
 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 postcondition x == n & y == m
, the equations must imply the postconditions.
 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.
 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 precondition through a program to the program’s postcondition. This approach is known as symbolic execution.
A MetaNotation 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 metanotation, 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 metanotation denotes collections of Slang programs by means of metavariables for which Slang expressions can be substituted. We distinguish metavariables, say "v" , from other objects by printing them as v . In the table below we introduce the metanotation for assignment and conditional and give an example for each.
Statement  Metanotation  Slang example 

ValDeclaration  val x = E  val m = n + 1 
VarDeclaration  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 metavariables in the table above are intended to be instantiated by specific syntactic Slang objects like variables or expressions. We consistently use a set of metavariable names as listed in the table below.
Metavariable  Intended instantiation 

x , y , z  Slang variables 
E , F  Slang expressions 
B , C  Slang Boolean expressions 
S , T  Slang (nonsequential) statements 
S1 , S2 , …, Sn  n Slang (nonsequential) statements, possible zero 
P , Q  Slang Blocks 
Remarks

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
S1S2⋮Sn 
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. 
Note, that a block is allowed to empty (for n = 0). An empty block does nothing. In case the elseblock 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 VarDeclaration
Substituting m for x and n + 1 for E in the metadeclarations, both val and var, we obtain the concrete Slang declarations on the righthand side. Each declaration contains an initial assignment of the newly declared variable. The declared Slang variable, here m , must not occur on the righthand side of the assignment. It is not known before its declaration.
Assignment
Substituting m for x and m + 1 for E in the metaassignment, we obtain the concrete Slang assignment on the righthand 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 metasequential, we obtain the concrete Slang sequential on the righthand side.
Block
Substituting x = x + y for S1 , y = x  y for S2 x = x  y for S3 , with n = 3, in the metablock, we obtain the concrete Slang block on the righthand side.
Conditional
Substituting x >= 0 for B , { y = x } for S and { y = x } for T in the metaconditional, we obtain the concrete Slang conditional on the righthand 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.