Given a simple if statement with the following general syntax,

if C then S

And without an else-part, the rule for calculating wp() is as follows.

    wp("if C then S" , R)

becomes

C ==> wp(S, R)   &&    ( not C ) ==> R

We want to prove the following. Let R be the following boolean expression,

forall x in i..n, A[j]>=A[x])

Now, we want to prove the following, and determine what value for precondition, Q, will ensure R is true after executing these statements.

assert(Q);
i = i - 1;
if A[i] > A[j] then j = i;
assert(R);

assert(Q);
i = i - 1;
if A[i] > A[j] then j = i;
assert(forall x in i..n, A[j]>=A[x]);

Since,

wp( "j = i",
    forall x in i..n, A[j]>=A[x] )
 = forall x in i..n, A[i]>=A[x]

We have,

wp( "if A[i] > A[j] then j = i",
    forall x in i..n, A[j]>=A[x] ) =

( ( A[i]>A[j] ) ==>
    forall x in i..n, A[i]>=A[x] )  &&
( ( A[i]<=A[j] )  ==>
    forall x in i..n, A[j]>=A[x] )

Simplifying,

( ( A[i]<=A[j] ) ||
  forall x in i..n, A[i]>=A[x] )   &&
( ( A[i]>A[j] )  ||
  forall x in i..n, A[j]>=A[x] )

An point (that will become interesting in a later example about loops) is that the postcondition imply the precondition simplified thus far. Inotherwords,

( forall x in i..n, A[j]>=A[x] ) ==>
  ( ( A[i]<=A[j] ) ||  forall x in i..n, A[i]>=A[x] )  &&
  ( ( A[i]>A[j] )  ||  forall x in i..n, A[j]>=A[x] )

Since R ==> Q, we may write,

assert(R);
i = i - 1;
if A[i] > A[j] then j = i;
assert(R);

Here is a review of the truthtable for ==>

There are other syntaxes for if statements. And each of these requires a different rule for WP() calculations. For example, with the following general syntax,

if C then S1 esle S2 end

And without an else-part, the rule for calculating wp() is as follows.

    wp("if C then S1 else S2 end" , R)

Becomes

C ==> wp(S1, R)   &&    ( not C ) ==> wp(S2, R)

Here is an example for COND.

(cond ((C1 S1)
       (C2 S2)
       ...
       (Cn Sn))

wp("(cond ((C1 S1)... (Cn Sn))",  R)

Becomes

C1 ==> wp(S1, R)   &&
( not C1 && C2 ) ==> wp(S2, R)  &&
      ...  &&
( not C1 && not C2 && ... && not Cn-1  && Cn)
 ==> wp(S2, R)

So the problem is that the wp gets way more complicated with each additional test. And this is because the way the guards are exectuted. COND executes them in sequence. So Sn only fires if all the conditions C1..Cn-1 were false and the last, Cn, is true.

Finially here is an example for Djikstra's guarded IF.

if C1 -> S1
[] C2 -> S2
     ...
[] Cn -> Sn
fi

wp("(cond ((C1 S1)... (Cn Sn))",  R)

Becomes

C1 ==> wp(S1, R)   &&
C2  ==> wp(S2, R)  &&
  ...  &&
Cn ==> wp(S2, R)

And the wp expansion is so much simpler than COND because of the semantics of the guarded IF. Non deterministic selection of guards allows for this.