Programming Notes – Statement Sequence
Let r and s be two program statements. The statement sequence
r;s
is also a program statement. The statement sequence has the meaning: activate statement r, then activate statement s.
Using the weakest precondition form, the semantics of the program sequence is
WP((r;s),R) = WP(r,(WP(s,R)).
Suppose that r and s also represent the relations formed by the respective activation of the program statements r and s. The following analysis starts with a definition of statement sequence based on the concepts related to the set-condition of a program statement sequence.
Preliminary Concepts
The symbols r and s represent two program statements and also represent the respective relations that define activation of the program statements. The composite statement
r;s
also has an associated relation identified as r;s. Activating two statements in sequence causes the result state of the first statement to be the initial state of the second statement. Proper termination of two successive program statements suggests that there must exist an intervening program state resulting from the activation of the first statement and guaranteeing successful termination of the second statement. Thus proper termination of two successive program statements suggests the existence of two ordered pairs a r y and y s b with the common element y.
The properties of relation compositions suggest the following axiom.
Theorem 2: WP.(r;s).R = WP.r.(WP.s.R)
Theorem 3: P {r} Q Ù S {s} R Ù Q Í S Þ P {r;s} R
Theorem 5: P {r;s} R º P {r} WP.s.R
Corollary: P {r;s} R º P {r} WP.s.R Ù WP.s.R {s} R
Theorem 6: P {r} Q Þ (P {r;s} R º P {r} (Q Ç WP.s.R))
Corollary: P {r} Q Þ (P {r;s} R º P {r} (Q Ç WP.s.R) Ù (Q Ç WP.s.R) {s} R)
The intermediate outcome Q may not be guaranteed per se in the following extension of Theorem 5.
Theorem 7: (P {r} WP.s.R º P {r} (QÇWP.s.R)) Þ
(P {r;s} R º P {r} (QÇWP.s.R) Ù (QÇWP.s.R) {s} R)
Theorem 8: (Associative Property) WP.((r;s);t).R = WP.(r;(s;t)).R
Two program statements are equivalent with respect to the weakest precondition of a third statement when the program statements may be interchanged in a program sequence.
Theorem 9: P {r} WP.t.R º P {s} WP.t.R º P {r;t} R º P {s;t} R
If two program statements form the same weakest precondition, then the program statements may be interchanged in a program sequence.
Theorem 10: WP.s.R = WP.t.R Þ P {r;s} R º P {r;t} R
Theorem 11: ("B|("A|A {r} B º A {a} B:A):B) Ù ("B|("A|A {s} B º A {b} B:A):B) Þ
("B|("A|A {r;s} B º A {a;b} B:A):B)
The strongest result connects two statements in a sequence in a way similar to the weakest precondition.
Programming Example:
An example of a program with a sequence of program statements is the switch2 program. Try the switch2 program and examine the program logic.
The switch2 program transfers the values of two text boxes without using an intermediate variable. The program verifies that the chosen values are integers, but the program would work as well with real numbers.
The key program statements in abbreviated form are:
s1: a = b – a
s2: b = b – a
s3: a = a + b
The expected result is
R = {a,b | a = b.valueÙ b = a.value}
The problem is to derive the set of conditions P that statisfies the Hoare Triple:
P {s1;s2;s3} R
The solution P uses a combination of Theorem 4 and Assignment Statement Theorem 3. Each of the assignment statements terminate for any number, so the domains will be ignored in the derivations. Theorem 4 uses two intermediate states and three Hoare Triples:
P {s1} Q1, Q1 {s2} Q2, Q2 {s3} R
The domains of each operation is the Universal set, sot Assignment Statement Theorem 3 specifies the following solutions to P, Q1, and Q2.
Q1[a := b – a] {s1} Q1
Q2[b := b – a] {s2} Q2
R[a := a + b] {s3} R
The solution process starts with the last Hoare Triple and works backward. First equate set Q2 to
Q2 = R[a := a + b]
The solution to the second Hoare Triple becomes
R[a := a + b][b := b – a] s2 R[a := a + b]
Similarly, the solution to the first Hoare Triple becomes
R[a := a + b][b := b – a][a := b – a] s1 R[a := a + b][b := b – a]
Theorem 4 suggests that the following Hoare Triple is a derivation of the solution.
R[a := a + b][b := b – a][a := b – a] {s1;s2;s3} R
Problems:
Examine the switch2 program example. After trying the program, view the source program code.
JavaScript treats text box values as strings, so the parseInt functions convert the text box strings to integer variables. Remove the parseInt references and try the program again. The program should not achieve the result R. Why not?
JavaScript supports the boolean exclusive-or operator ^. Since integers are represented in a computer as binary numbers, the exclusive-or operator is a valid integer operator. The exclusive-or operations are
1^0 = 0^1 = 1
1^1 = 0^0 = 0
If a, b, and c are integers, then the following exclusive-or operations are valid
a^0 = 0^i = a
a^a = 0.
a^b = b^a
a^(b^c) = (a^b)^c
Based on the arithmetic rules for the exclusive-or operator, write a new version of the switch2 program that uses exclusive-or operators instead of addition and subtraction.
The condition of the statement
i = Math.random() * b
is derived in the assignment statement analysis. The following statement sequence is an equivalent form:
r = Math.random()
i = b * r
Using the assignment statement analysis as a model, derive the condition of the program sequence shown above.
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Fejer, Peter A., 1991, Mathematical foundations of computer science, New York, NY: Springer-Verlag
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
http://www.anaesthetist.com/mnm/javascript/index.htm Chapter 2 contains an excellent description of boolean operations in JavaScript.