Programming Notes – Quantifying Sequences
Let
r and s be two program statements. The
statement sequence
r;s
is
also a program statement. For an introduction to program statement
sequences, see Statement Sequences.
Sequence
as Operator
The
sequence operator (;} combines two program statements to form a new program
statement. The new program statement
may be used as a part of a program solution as described in Weakest Preconditions and in Programming
Solutions.
Quantification of sequences
A sequence of
may contain more than two program statements, and some program sequences may
contain zero program statements. In both cases, a quantifying expression
may be appropriate.
sequence = (;x|E:r[x])
The expression E
defines the scope of the quantifying variable x. The expression r[x] represents either a program statement or
a predicate. The variable x often represents the ordinal value of the
expression r[x]. Program
sequences are enclosed in braces {} instead of parentheses. In the sequence expression
(;x|0£x£5:r[x])
the third
statement in the sequence may be represented as r[2].
Properties of Program Sequences
The properties
of program sequences correspond to the properties of program solutions in the
form of Hoare Triples and weakest preconditions.
The program
sequence operator has an identity as shown in Program
Skip Theorem 5 and 6. The program sequence is associative as shown in
Program Sequence Theorem 8. The
program sequence is not symmetric, and many properties of quantifying
statements do not apply. Because the program sequence is not symmetric,
maintaining ordinality of each program statement in the sequence is important,
for example. Similarly, distributive rules do not, in general, apply
because program statement ordinality would be affected.
A quantifying statement
of the form
(;i|m£i£n:B[i])
is appropriate,
because the quantifying variable i determines ordinality of B[i].
The empty
program statement ‘ ‘ may be represented by the quantifying statement
Null = (;x|false:B[x]).
A quantifying
statement with an empty range is equivalent to the identity value, so a program
statement sequence over an empty range is equivalent to the skip statement.
Axiom 1: P {skip} R º P {(;x|false:B[x])}
R
A program
sequence may be split into smaller sequences as long as the ordinality is
maintained and no duplication of program statements occurs.
Axiom 2: (RÇS = ÆÙ (iÎR Ù jÎS º
B[i]<B[j])) Þ
(;x|RÈS:B[x])
= (;x|R:B[x]);(;x|S:B[x])
Suppose that RÈS = m£i£n, and the integer k is
such that m£k£n. Then
(;|m£i£n:B[i]) = (;|m£i£k:B[i]);(;|k<i£n:B[i])
When the
quantifying variable points to one state, that state determines the program
statement.
Axiom 3: P {(;x|x=E:B[x])} R º P
{B[E]} R
Activation of a quantifying
statement
Program
statements may be activated. Thus
A((;x|0£x£5:r[x]))
represents the
activation of the six program statements
A(r[0]; r[1]; r[2]; r[3]; r[4]; r[5]).
The activation
of a statement sequence should be the successive activation of each
statement. So activation should distribute over the sequence operator.
Axiom 4:
A((;x|E:r[x])) º (;x|E:A(r[x]))
Program Statement Theorems
The skip
statement is the program sequence identity. A sequence of skip statements
should be equivalent to one skip statement.
Theorem
1: P {(;x|m£x£n:skip)} R º P {skip} R
Program Sequence Theorem 4 may be generalized
so that it applies to a sequence containing more than two statements.
Theorem 2: ("n|k£n: ("i|k£i£n:
H[i-1] {r[i]} H[i]) Þ
H[k-1] {(;i|k£i£n: r[i])}
H[n]
Program Sequence Theorem 11 may be
generalized so that it applies to a sequence containing more than two
statements.
Theorem 3: ("i|k£i£n:("B|("A|A {r[i]}
B º A {s[i]} B:A):B)) Þ
("B|("A|A {(;i|k£i£n:r[i])}
B º A {(;i|k£i£n:s[i])} B:A):B)
A special case of Theorem 3 occurs when each
program statement r[i] represents the same program statement r, and each program statement s[i] represents the
same program statement s.
Theorem 4: ("B|("A|A {r} B º A {s}
B:A):B) Þ
("B|("A|A {(;i|k£i£n:r)}
B º A {(;i|k£i£n:s)} B:A):B)
Example:
The evaluation of the
Hoare Triple
P {(;i|0£i£n:x := x+1)} R
uses the sequence quantification
axioms and the principles of induction. The evaluation relies on the solution
to the assignment statement as shown in Assignment
Statement Theorem 3 and the solution to a sequence as shown in Program Sequence Theorem 4.
The program sequence
suggests the solution
P {(x := x + n + 1)} R
First, evaluate the Hoare
Triple for case n=0.
P {(;i|0£i£0:x := x+1)} R
º(algebra)
P
{(;i|i=0:x := x+1)} R
º(one point rule)
P {x := x+1} R
º(algebra)
P {x := x+0+1} R
The solution for (x :=
x+1) is:
R[x := x+1] {x := x+1} R
The corresponding
solution for (;i|0£i£k:x := x+1) is, according to
the induction assumption:
R[x := x+1][x := x+k+1] {(;i|0£i£k:x := x+1)} R[x := x+1]
Suppose R = {the
assignment value is x}.
Evaluation of R[x :=
x+1][x := x + k + 1]:
R[x
:= x+1]= {the assignment value is x+1}
R[x
:= x+1][x := x + k + 1]= {the assignment is x+k+1+1}
The evaluation of R[x :=
x+1][x := x + k + 1] yields the expected result.
Problems:
Show
that the statement
P {(;i|0£i£n:x=x+x)} R
is
equivalent to
P {x := 2(n+1) * x} R
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.