Programming Notes – Assignment Statements
The assignment statement has the form
x := E
where x is a variable and E is an expression.
Dijkstra defines, in the general case, the semantics of the assignment statement using the weakest precondition form:
WP(‘x := E’, R) = R[x := E] Ù domain(E).
The following analysis shows that the Hoare Triple form of the assignment statement:
(R[x := E] Ç dom.(x := E)) {x := E} R.
Preliminary Concepts
Analysis of the assignment statement depends on the concept of a point in a state space. Prelilinary state space concepts are found in Program States Part 1.
Let E be an expression and let s be an arbitrary point such that:
s = {<’x’, Sx>, <’y’, Sy>, ×××,<’z’, Sz>}
Activation of the assignment statement
x := E
causes the value of the variable x to be replaced by the value of expression E at point s resulting in the point t
t = {<’x’, E[s]>, <’y’, Sy>,×××, <’z’, Sz>}
Thus activation of the assignment statement may be described by the first axiom.
Axiom 1: s (x := E) t º t = {<’x’,E[s]>,<’y’,Sy>,×××,<’z’,Sz>}
s (x := E) t º t = {<’x’,E[s]>,(,i|1£i£m:<’t.i’,Ss.i>)}
In Axiom 1, the expression s (x := E) t is a member of the relation corresponding to the set ordered pairs satisfying describing activations of the program statement {x := E}.
Ordered pairs in the relation (x := E) have general properties. If <s,t> is a member of the relation formed by (x := E), then t being a member of R is equivalent to s being a member of R[x := E].
Theorem 1: s (x := E) t Þ t Î R º s Î R[x := E]
Corollary: s (x := E) t Ù s Î R[x := E] Þ t Î R
Corollary: s (x := E) t Ù t Î R Þ s Î R[x := E]
Theorem 2: ran.(x := E).R[x := E] Í R
Theorem 3: (R[x :=E] Ç dom.(x := E)) {x := E} R
If the assignment statement teminates normally for all program states, then the domain can be omitted from the Hoare Triple.
Theorem 4: dom.(x := E) = U Þ R[x :=E] {x := E} R
R[x := E] has properties with respect to the domain of R. First, the domain of R is a subset of R[x := E].
Theorem 5: dom.(x := E).R Í R[x := E]
When R[x := E] is a subset of the domain, then R[x := E] is also a subset of the domain of R. That is, when all members of R[x := E] lead to a correct calculation, then activation leads to a result in set R.
Theorem 6: R[x := E] Í dom.(x := E) Þ
R[x := E] Í dom.(x := E).R
When R[x := E] is a subset of the domain, it follows that R[x := E] is the domain of R.
Theorem 7: R[x := E] Í dom.(x := E) Þ R[x := E] = dom.(x := E).R
Theorem 8: R[x := E] Í dom.(x := E) Þ R[x := E] = WP.(x := E).R
The assignment of a properly typed constant leads to the result that the assigned variable has a value equal to the constant.
Theorem 9: Given K is a constant of consistent type for Prog.x,
U {x := K} {State.s|: Prog.x = K}
Similarly, the assignment of a properly typed constant has a weakest precondition equal to the universal set.
Theorem 10: Given K is a constant of consistent type for Prog.x,
WP.(x := K).{State.s|: Prog.x = K} = U
When the expression being assigned is a function, then the relation formed by the program statement is also a function.
Theorem 11: E is a function over the weakest precondition Þ {x := E} is a function over the weakest precondition.
Suppose that the expected result R means that the absolute value of the program variable x is greater than 5.
R = {State.b| |x| > 5: State.b}
The program statement r is ‘x := 5/y’, and the problem is to determine a solution.
First, evaluate R[x := 5/y]:
R[x := 5/y] = {State.b| |5/y| > 5: State.b}
R[x := 5/y] = {State.b| 5/|y| > 5: State.b}
R[x := 5/y] = {State.b| 5/5 > |y|: State.b}
R[x := 5/y] = {State.b| 1 > |y|: State.b}
Second, derive dom.’x := 5/y’.
dom.’x := 5/y’ = {State.b| y ¹ 0: State.b}
The solution is R[x := 5/y Ç dom.’x := 5/y’.
solution = {State.b| 1 > |y|: State.b} Ç {State.b| y ¹ 0: State.b}
solution = {State.b| 1 > |y| Ù y ¹ 0: State.b}
Analysis of assignment statements involves the derivation of R[x := E] Ç dom.’x := E]. One approach is to derive the specifications of R[x := E] from the expected result R, then to remove any points in which the expression E does not evaluate correctly.
The randomizing program example has an interesting assignment statement because of the random number function in the assignment statement. The specific return value of the random number function cannot be predicted unless the algorithm is known, and the initial values of the respective variables are not known. So the program may be viewed as a black box.
The randomize program returns a random number that is used as a subscript in an array of check boxes. The array is simply called ‘array’. The number of elements in the array is denoted by array.length. Valid subscript values range from 0 to array.length – 1. In JavaScript, a real number may be used as the subscript of an array. The integer part of the subscript denotes the referenced element of the array.
The random number function available in JavaScript is Math.random(). The random number function in JavaScript returns a number 0 < r < 1. Multiplying the random number by an integer b returns a number that may be used as a subscript value in the range
0 £ r×b < b.
The key statement in the randomize program is
r = ‘i = Math.random() * b’
Activation of r should lead to the expected result: the variable i should represent an integer 0 £ i < array.length.
R = {State.t | 0 £ i < array.length}.
Theorem 3 suggests that R[i := Math.random()×b] Ç dom.’i = Math.random()*×b’ represents a solution to program statement r.
R[i := Math.random()×b] =
{State.t | 0 £ Math.random()×b < array.length}
The program statement r evaluates correctly for all values of b, so the domain is the set of states where the variable b is a number. The set R[i := Math.random()×b] is therefore a solution to the assignment statement. Unfortunately, the random number generated by Math.random() must be constrained by the value of the program variable b. The value of Math.random() cannot be predicted, so this problem is an example of a ‘black box’ where some initial values are not known.
One solution to the black box problem is to add another constraint that takes all possible values of the black box variable into consideration. In the assignment statement shown above, the parameter b should be large enough so that all integer values 0 £ i < array.length should be possible, so array.length £ b. The expected result R becomes
R = {State.t | 0 £ i < array.length Ù array.length £ b}.
The solution set R[i := Math.random()×b] becomes
R[i := Math.random()×b] =
{State.t | 0 £ Math.random()×b < array.length Ù array.length £ b}
The specific value of the random number function is not known, but the range of possible values is known. The Math.random() function returns a value 0 < r < 1.
R[i := Math.random()×b] =
{State.t | 0 £ Math.random()×b < 1×b £ array.length Ù array.length £ b}
The value of b may now be determined.
{State.t | 0 < ×b £ array.length Ù array.length £ b}
It follows that a solution to statement r occurs when b = array.length.
Problems:
In the randomizing program, remove the guarding statement that prevents generating invalid subscripts and run the program.
The domain and solution to the random number assignment problem are interesting sets. One may create a graphical representation using a Cartesian coordinate graph. Let the horizontal line be various values of the variable b, and let the vertical line be various values of the random number. Draw a line representing the highest allowable value of the random number for each value of b. The area under the graph is a representation of the domain and the general solution. Shade the area under the graph representing the final, specific solution. Explain why the specific solution is a subset of the domain. Using the graph as a reference, explain why the value of b should be limited to the array length.
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