Programming Notes – Program if-statements – Guarded Commands
Introduction
The Dijkstra model of the if-statement summarized in if-statements part 1 offers an elegant programming solution, but Dijkstra’s description of the weakest precondition
WP(IF,R) = ($i | 0£i£n : B[i]) Ù ("i | 0£i£n : B[i]ÞWP(S[i],R))
is ambiguous in an interesting way. Does the expression B[i]ÞWP(S[i],R) describe a characteristic of the weakest precondition or does the expression B[i]ÞWP(S[i],R) describe a characteristic of the if-statement? The analysis on this page and in Guarded Command Sequences suggests that the if-statement solution is best described by the conditions B[i].
This page describes one element of the Dijkstra if-statement: the guarded command. The next page describes the if-statement as a special sequence of guarded commands. The solutions parallel very closely with Dijkstra’s presentation, but the flavor is very different.
The guarded command is defined as
The Guard B prevents activation of the guarded statement r when the condition B is not true in the current program state. The set B, known as the guarding set, represents all program states in which the condition B is true. When the current state is in the set B then activation of the statement r occurs, and the guarded command behaves like the statement r. When the current state is not in the set B then activation of the statement r does not occur, and the guarded command behaves like a skip statement.
In modern computer languages, the language segments corresponding to guards sometimes also change the program state. In Dijkstra’s model and in this model, the guard does not change the program state.
Guarded commands can be nested. The nested guarded command
A®(B®r)
has two guards: A and B. The guard A is the outer guard. The outer guard has a corresponding outer guarding set A. The guard B is the inner guard. The inner guard has a corresponding inner guarding set B. The nested guarded command may be written as
A®s,
where s corresponds to the guarded command
B®r.
The following two axioms describe how solutions to a guarded command may be derived from solutions of the guarded statement. The first axiom describes a solution when the precondition is a subset of the guard set. The second axiom describes a solution when the precondion is a subset of the guard set’s complement. Every singleton set is either a subset of the guard set or a subset of its complement (Singleton Set Theorem 4), so every single program state falls under Axiom 1 or Axiom 2.
Axiom 1: (Guarded Command Solution) PÍ B Þ P {B®r} R º P {r} R
Axiom 2: (Guarded Command Solution) P Í ~B Þ P {B®r} R º P {skip} R
Sequence of Guarded Commands
A sequence of guarded commands can represent a single program statement. In a sequence each guard is identified based on the order the guard appears in the sequence. Each guarded statement is identified based on the identification of the associated guard. A sequence of guarded commands may be denoted as:
Definition 1: GC[k,n] = (;i|k£i£n:B[i]®r[i])
Guarded Command Theorems
The following theorems derive guarded command solutions by applying the guarded command axioms to the weakest precondition theorems and axioms.
Applying the first axiom and the weakest precondition axiom leads to the general solution for a guarded command.
Theorem 1: B Í WP.r.R Ù P Í B Þ P {B®r} R
A set is a subset of itself, leading to the special case that the guarding set represents a solution to the guarded command.
Theorem 2: B Í WP.r.R Þ B {B®r} R
A variation of the second theorem is shown below.
Theorem 3: B Í WP.r.R Þ B Í WP.(B®r).R
Any set intersecting with the guarding set forms a solution to a guarded command through the application of Axiom 1.
Theorem 4: (P Ç B) {B®r} R º (P Ç B) {r} R
Any set intersecting with the guarding set’s complement forms a solution to a guarded command through the application of Axiom 2.
Theorem 5: (P Ç ~B) {B®r} R º (P Ç ~B) {skip} R
Theorem 6: ~B {B®r} R º ~B {skip} R
If the guarding set’s complement is in the precondition, then the program state does not change.
Theorem 7: RÇ~B {B®r} RÇ~B
Corollary: RÇ~B {B®r} ~B
Corollary: RÇ~B {B®r} R
If guarding set is a subset of the guarded statement’s weakest precondition then the weakest precondion is the guarding set in union with the result set.
Theorem 8: B Í WP.r.R Þ WP.(B®r).R = BÈR
When a program statement has nested guards and the interior guard is a subset of the guarded statement’s weakest precondion, then any subset of the guarding sets’ intersection is a solution to the nested guarded command.
Theorem 9: B Í WP.r.R Ù P Í A Ç B Þ P {A®(B®r)} R
When a program statement has nested guards, then any subset of the intersection between the outer guarding set and the interior guard’s complement forms a solution equivalent to that of the skip statement.
Theorem 10: P Í A Ç ~B Þ P {A®(B®r)} R º P {skip} R
As a special case of Theorem 10, any further intersection between the outer guarding set and the inner guarding set’s complement also forms a solution equivalent to that of the skip statement.
Theorem 11: (P Ç A Ç ~B) {A®(B®r)} R º (P Ç A Ç ~B) {skip} R
The property shown in Theorem 5 may be extended to a guarded command sequence. If all of the guards of a guarded command sequence are false, then the guarded command sequence behaves like the skip statement.
Theorem 12: (P Ç (Ç|k£i£n:~B[i]) {GC[k,n]} R º
(P Ç (Ç|k£i£n:~B[i]) {skip} R
When a guard is always true, then the guard serves no purpose except to be a place-holder. The guard ‘true’ is a place-holder guard.
Theorem 13: P {true®r} R º P {r} R
When a guard is always false, then the guarded command behaves like the skip command. The guard ‘false’ is a skip guard.
Theorem 14: P {false®r} R º P {skip} R
Mapping the guarded command into a JavaScript format
Guarded commands may be implemented in JavaScript using simple JavaScript if-statements.
(B ®r) º {if (B) r;}
The guard in the guarded command corresponds to the boolean expression in the JavaScript if-statement, and the guarded statement in the guarded command corresponds to the imperative statement in the JavaScript if-statement.
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.