Programming Notes – if-statement - Weakest Preconditions

 

A guarded command consists of a conditional expression also called the guard and an imbedded statement that is activated when the guard is true.  The guarded command has the syntax

 

      B à S

 

where B is the guard and S is the imbedded statement.

 

A control statement contains a sequence of zero or more guarded commands.  The two basic forms of the control statemenr are the if-statement and the do-statement.  The different control statement forms share a similar syntax, and the semantics of the do-statement are a simple extension to the semantics of the if-statement.  This page and the next page describe if-statements in the weakest precondition form and the set-condition form.

 

Let B be an array of conditional expressions, and let S be an array of program statements.  A sequence of guarded commands may be formed by associating the nth guard with the nth program statement.  Thus

 

      B[i] à S[i]

 

forms one of the guarded commands.

 

Activation of the guarded command ‘B[i] à S[i]’ may be described as

 

      B[i] Þ activation of S[i].

 

One can build an if-statement from the sequence of guarded commands:

 

      IF = ‘if B[0] à S[0] || B[1] à S[1] || ¼ B[n] à S[n] endif’

 

Activation of an if-statement may be described as the successive activations of the guards until either all the guards have been activated or one of the guards is true.  Dijkstra defines the weakest precondition of the if-statement as

 

      WP(IF,R) = ($i | 0 £ i £ n : B[i]) Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

 

Dijkstra points out an interesting implication of his definition of the if-statement weakest precondition.  When all B[i] are false, then the if-statement should not have a resulting state.  That is, when all B[i] are false, the if-statement is semantically equivalent to the abort statement.

 

Theorem 1: ("i | 0 £i £n : ØB[i]) Þ WP(IF,R) = false

(given that ("i | 0 £i £n : ØB[i])

(definition of WP(IF,R)

WP(IF,R) = ($i | 0 £ i £ n : B[i])

Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))   

º(identity of Ù)

      WP(IF,R) = ($i | 0 £ i £ n : B[i])

Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

Ù true

Þ(substitution) 

      WP(IF,R) = ($i | 0 £ i £ n : B[i])

Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

Ù("i | 0 £i £n : ØB[i])

º(symmetry and associativity of Ù)

WP(IF,R) = (($i | 0 £ i £ n : B[i]) Ù("i | 0 £i £n : ØB[i]))

Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

º(DeMorgan)

WP(IF,R) = (($i | 0 £ i £ n : B[i]) ÙØ($i | 0 £i £n : B[i]))

Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

º(p ÙØ p º false)

WP(IF,R) = false Ù ("i | 0 £ i £ n : B[i]Þ WP(S[i],R))

º(zero of Ù)

WP(IF,R) = false 

End of Proof

 

The empty if-statement ‘if endif’ is semantically equivalent to the abort statement.

 

Theorem 2: WP(‘if endif’, R) º false

(Definition of WP)

      WP(‘if endif’, R) º

($i | false: B[i]) Ù ("i | false: B[i]Þ WP(S[i],R))

º(empty range)

      falseÙ true

º(identity of Ù)

      false

End of Proof

 

 

A programming problem:

Write an adder program that adds or subtracts argument b from argument a depending on the value of argument c.  The program should accept three arguments, two objects that have a ‘value’ property and one string argument.  The values of arguments a and b are positive integers, and the value of argument c is ‘+’, ‘-‘, or some other value.  If argument c is not ‘+’ or ‘-‘ then no operation should be performed.

 

The expected result R is

 

      R = (c = ‘+’ Ù a.value = a.value + b.value)

           Ú (c = ‘-’ Ù a.value = a.value - b.value)

           Ú (c ¹ ‘+’ Ù c ¹ ‘-’ Ù a.value = a.value)

 

Let B[0] be “c = ‘+’”, and let S[0] be “a.value = a.value + b.value”.

Let B[1] be “c = ‘-’”, and let S[1] be “a.value = a.value - b.value”.

Let B[2] be “c ¹ ‘+’ Ù c ¹ ‘-’”, and let S[2] be “skip”.

 

It can be shown that

 

      ($i|0£i£2:B[i]) Ù ("i|0£i£2:B[i] Þ WP(S[i],R))

 

Thus, activation of the related if-statement will have the expected result R, leading to the following program.

 

function adder (a, b, c)

Begin

if

   c = ‘+’ à a.value := a.value + b.value

|| c = ‘-’ à a.value := a.value - b.value

|| c ¹ ‘+’ Ù c ¹ ‘-’ à skip

endif

end

 

Problems:

Show that each implication in ("i|0£i£2:B[i] Þ WP(S[i],R)) is true.

 

Show that ($i|0£i£2:B[i]) is true.

 

References:

 

Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall

 

Gries, David, 1981, The Science of Programming, New York, NY: Springer-Verlag

 

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag