1 Conditional Branches
1.1 Conditional Branches
Conditional Branches Conditional Branches
Slide 1
Conditional Branches
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 1/9
1
Conditional Branches Conditional Branches
An Example Program with Conditional Branches
1 int biggest(int x, int y, int z) {
2 // PRE: true (P )
3 // POST: r = max{x, y, z} (Q)
4 int res;
5 if (x >= y){
Slide 2
6 res = x;
7 } else {
8 res = y;
9 }
10 // MID: res = max{x, y} (M1 )
11 if (z >= res){
12 res = z;
13 }
14 // MID: res = max{z, max{x, y}} (M2 )
15 return res;
16 }
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 2/9
The code above does not modify the input parameter x, so you do not need to distinguish
between x, xpre or xold throughout. Similarly for y and z.
When choosing the mid-condition on line 13, you need to be careful with what you write.
One common mistake we have seen in the past is to write something like:
res = max{res, z}
Recall that this is a logical assertion and not code. The above does not describe an
assignment to the variable res, but rather makes a claim about its value being equal
to that of the larger of res or z. This can only be true if res ≥ z (i.e. we guarantee
that max{res, z} returns res) which is obviously not general enough for our proof as the
method’s pre-condition places no constraints on the input values of x, y or z.
Another common mistake is to write something like:
res = max{resold , z}
This describes the current value of res in relation to some program variable resold , but
there is no such variable in our code. Remember that we only use the old annotations in
our proofs to distinguish between the values stored in a variable before/after some code
has run. Such annotations have no place in our assertions.
2
Conditional Branches Conditional Branches
Proof Obligations
The choice of mid-conditions leads to the following proof obligations:
P ∧ if (x >= y){res = x;}else{res = y;} −→ M1
true ∧ res = max{x, y} −→ res = max{x, y}
Slide 3
M1 [res 7→ resold ] ∧ if (z >= res){res = z;} −→ M2
resold = max{x, y} ∧ res = max{z, resold } −→ res = max{z, max{x, y}}
M2 ∧ return res ; −→ Q[x 7→ xpre , y 7→ ypre , z 7→ zpre ]
res = max{z, max{x, y}} ∧ r = res −→ r = max{xpre , ypre , zpre }
(Don’t forget x = xpre ∧ y = ypre ∧ z = zpre throughout this program)
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 3/9
Conditional Branches Conditional Branches
Reasoning about Conditional Branches
How do we prove that branching code satisfies its specification?
1 // PRE: P
2 if (cond){
3 code1;
4 } else {
Slide 4
5 code2;
6 }
7 // POST: Q
Using P and the case of cond as assumptions we have to show that Q
holds after executing each branch code1 and code2.
{ P ∧ cond } code1 { Q } { P ∧ ¬cond } code2 { Q }
{ P } if(cond){ code1 } else { code2 } { Q }
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 4/9
Notice above that there is a slightly unfortunate clash between the syntax of our pro-
3
gramming language and that of our proof system, both making use of curly-brackets { }.
In the code, these delimit the scope of our conditional and looping statements, whereas
in the proof system there separate the assertions from the code. We have to take a little
care not to get confused by this symbolic overloading.
Conditional Branches Conditional Branches
Reasoning about Conditional Branches
We can introduce appropriate mid-conditions to guide our proof:
1 // PRE: P
2 if (cond){
3 // MID: P ∧ cond
4 code1;
Slide 5
5 // MID: R1
6 } else {
7 // MID: P ∧ ¬cond
8 code2;
9 // MID: R2
10 }
11 // POST: Q
code1 and code2 may “assume” P and their respective case for free.
It is the “responsibility” of both code1 and code2 to establish Q
(i.e. R1 −→ Q and R2 −→ Q).
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 5/9
When reasoning about a conditional branch we get to assume that the pre-condition holds
at the start of each branch. We also get to assume that the condition cond holds in the
then branch and does not hold in the else branch.
We then have to show that the post-condition holds after running either branch of the
code. We can either do this directly at the end of each branch (i.e. establish Q as in
the rule) or we can show that the mid-condition at the end of each branch implies the
post-condition Q (as we have structured things in the slide above). This latter approach
can be helpful to break down the complexity of our proofs.
It is possible that P ∧ cond −→ false or P ∧ ¬cond −→ false. Whilst this might seem
like a problem, it actually just means that one branch or the other is unreachable. We
can carry false through our mid-conditions (the triple {false} code {false} is always
true) and then the proof obligation at the end of the branch becomes false −→ Q which
holds trivially.
4
Conditional Branches Conditional Branches
Conditional Branches - Example
Looking at the first part of our biggest method in more detail:
1 // PRE: true (P )
2 int res;
3 if (x >= y){
Slide 6
4 // MID: x ≥ y (P ∧ cond)
5 res = x;
6 // MID: res = x ∧ x ≥ y (R1 )
7 } else {
8 // MID: y > x (P ∧ ¬cond)
9 res = y;
10 // MID: res = y ∧ y > x (R2 )
11 }
12 // MID: res = max{x, y} (M1 )
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 6/9
We are assuming that this code snippet exists in a program where the variables x and y
have been declared, otherwise the program would not even compile.
5
Conditional Branches Conditional Branches
Proof Obligations
The choice of mid-conditions leads to the following proof obligations:
P ∧ cond ∧ res = x; −→ R1
x ≥ y ∧ res = x −→ res = x ∧ x ≥ y
Slide 7
R1 −→ M1
res = x ∧ x ≥ y −→ res = max{x, y}
P ∧ ¬cond ∧ res = y; −→ R2
y > x ∧ res = y −→ res = y ∧ y > x
R2 −→ M1
res = y ∧ y > x −→ res = max{x, y}
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 7/9
Note that if we had used M1 for both R1 and R2 , then we would only have two proof
obligations:
P ∧ cond ∧ res = x; −→ M1
x ≥ y ∧ res = x −→ res = max{x, y}
and
P ∧ ¬cond ∧ res = y; −→ M1
y > x ∧ res = y −→ res = max{x, y}
Whilst this would clearly be simpler in this case, in general our conditional branches
might not be so similar. In fact, it is quite common for the mid-condition after the
conditional branch to be a disjunction of the effects of each branch.
6
Conditional Branches Conditional Branches
Conditional Branches - Example
Looking at the second part of our biggest method in more detail:
Slide 8
1 // MID: res = max{x, y} (M1 )
2 if (z >= res){
3 // MID: res = max{x, y} ∧ z ≥ res (M1 ∧ cond)
4 res = z;
5 // MID: res = z ∧ z ≥ max{x, y} (R3 )
6 }
7 // MID: res = max{z, max{x, y}} (M2 )
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 8/9
We are assuming that this code snippet exists in a program where the variables x, y and
z have been declared, otherwise the program would not even compile.
Notice that we do not need a mid-condition for the (non-existent) else branch, although
we will still have a proof obligation that covers this case.
7
Conditional Branches Conditional Branches
Proof Obligations
The choice of mid-conditions leads to the following proof obligations:
(M1 ∧ cond)[res 7→ resold ] ∧ res = z; −→ R3
resold = max{x, y} ∧ z ≥ resold ∧ res = z −→ res = z ∧ z ≥ max{x, y}
Slide 9
R3 −→ M2
res = z ∧ z ≥ max{x, y} −→ res = max{z, max{x, y}}
M1 ∧ ¬cond −→ M2
res = max{x, y} ∧ z < res −→ res = max{z, max{x, y}}
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 9/9
The last proof obligation above corresponds to the execution path that does not enter
the conditional branch.