Programming Notes – Guarded Command Sequences Part 1
The if-statement is an alternative construct that follows the if-then-else pattern. That is, a true guard invokes the true-branch. Alternatively, a false guard invokes the else-branch. The following pages derive solutions to the if-statement based on an equivalent sequence of guarded commands. The alternative nature of the if-statement is achieved by introducing a flag variable that controls activation of guarded commands.
This page lists the definitions and axioms for the if-statements and guarded command sequences. The page shows some basic theorems about a sequence of guarded commands that will form a basis for if-statement theorems in subsequent pages.
Guarded Command Sequence Definitions
The solution for if-statements uses an equivalent sequence of guarded commands in which a flag variable plays in important role. The flag variable controls activation in a way that simulates the alternative construct.
A special guarded command sequence (G[k,n]) may be formed by nesting each guarded command inside another guarded command in which the the outer guard is the flag variable. When the flag is true and the guard B[i] is true, subsequent guards will not activate, because the flag variable is set to false. The sequence operator is appropriate in definition 1, because G[k,n] represents the activation of guarded commands in a sequence.
Definition 1: G[k,n] = (;i|k£i£n:(flag®(B[i]®(flag:=false;r[i]))))
An empty guarded command sequence (G[false]) may be forming an empty sequence of guards as described in definition 3.
Definition 2: G[false] = (;i|false:(flag®(B[i]®(flag:=false;r[i]))))
Guarded Command Sequence Theorems
The following theorems describe some of the characteristics of a guarded command sequence of the form G[k,n] as defined in definitions 1 and 2.
Given that the flag is true and all the guards are false, then the sequence of guarded commands is equivalent to the skip statement. The corresponding Hoare Triple solution follows directly from the theorem.
Theorem 1: (P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i])) {G[k,n]} R º
(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i])) {skip} R
Corollary: (P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))
{G[k,n]}
(P Ç {s|flag=true}Ç (Çi|k£i£n:~B[i]))
If the flag is false, then the sequence of guarded commands is equivalent to the skip statement.
Theorem 2: (P Ç {s|flag=false}) {G[k,n]} R º
(P Ç {s|flag=false}) {skip} R
A false flag and the weakest precondition of a sequence of guarded commands equals the false flag coupled with the weakest precondition of the skip statement.
Theorem 3: ({s|flag=false} Ç WP.G[k,n].R) = ({s|flag=false} Ç WP.skip.R)
The weakest precondition formed by the sequence of a flag assignment and a guarded statement equals the weakest precondition of the guarded statement.
Theorem 4: WP.(flag:=false;r).(RÇ{s|flag=false}) = WP.r.R
The relationship between the guard and the weakest precondition of the guarded statement implies the truth of the special guarded command used in if-statements.
Theorem 5: B[j] Í WP.r[j].R Þ
(PÇB[j] Ç{s|flag=true}) {G[j,j]} (R Ç{s|flag=false})
A set of solutions to the special sequence of guarded commands occurs when there is a true flag and a true guard and false prior guards. There is a member of the set of solutions corresponding to each guard in the sequence of guarded commands.
Theorem 6: ("i|k£i£n:B[i] Í WP.r[i].R) Þ
("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} (RÇ{s|flag=false}))
Corollary: ("j|k£i£n:B[j] Í WP.r[j].R) Þ
("j|k£j£n:({s|flag=true} Ç B[j] Ç (Çi|k£i£ j-1:~B[i])) {G[k,n]} R
Similarly, a true flag and the union of true guards forms a solution to the special sequence of guarded commands.
Theorem 7: k£n Ù ("j|k£j£n:B[j] Í WP.r[j].R) Þ
{s|flag=true} Ç (Èj|k£j£n:B[j]) {G[k,n]} (RÇ{s|flag=false})
Setting a flag variable prior to activating a sequence of guarded commands is equivalent to having the flag true as a precondition of the guarded command sequence.
Theorem 8: (P Ç {s|flag=true:s}) {G[k,n]} R º P {flag := true;G[k,n]} R
Mapping the guarded command sequence into a JavaScript format
The version of the if-statement analyzed on this page is a variation of Dijkstra’s model of the if-statement. Programming languages implement their own variations of the basic if-statement, but the general approaches are similar.
The JavaScript language implements an if-statement that has the same look and feel as the if-statement used in the Java language. In this section, the if-statement developed on this page is compared to the if-statement used in JavaScript. To differentiate between the two forms, the if-statement used in JavaScript programs is denoted as a JavaScript if-statement, and the if-statement of theory is denoted simply as the if-statement.
The analysis of guarded commands describes guarded command as a simple JavaScript if-statement. A sequence of guarded commands is simply a sequence of simple JavaScript if-statements.
(B[0] ®r[0]);(B[1] ®r[1]) º {if (B[0]) r[0]; if (B[1] r [1];}
The guarded command programming example demonstrates the how a sequence of simple JavaScript if-statements behave like a sequence of guarded commands.
The first scriptlet is an example of a single guarded command. Activation of the guarded command changes the program state when the guard is true.
The second scriptlet is an example of a sequence of guarded commands. In the example, each guarded command changes the program state because each guard is true at the time of activation.
Experiment with the scriptlets by modifying them and executing them under different scenarios.
Problems:
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
http://developer.netscape.com - Netscape's JavaScript Guide, Reference, and more
http://msdn.microsoft.com/workshop - Microsoft's JScript, DHTML info, etc.