Programming Notes – if-statement Solution Part 1
Though the set-model of if-statement semantics is very similar to the weakest-precondition model of if-statement semantics, the set-model goes in a distinctly different direction. First, the set-model uses a set-based weakest precondition, WP.if.R. Second, the set-model relaxes the constraint that at least one guard must be true. Third, a theorem shows that, according to the axioms and definitions, the empty form of the if-statement
‘if endif’
is equivalent to the skip statement. Equivalency of the skip statement is a result of defining the if-statement as a sequence of guarded commands. An empty sequence is equivalent to the skip statement, leading to the interesting conclusion that the empty if-statement is also equivalent to the skip statement.
The if-statement with all false guards is also made equivalent to the skip statement; a characteristic that will prove useful when the do-statement is defined as a special sequence of a repeating if-statement.
if-statement definitions and axiom
An if-statement has a special form unlike most program statements, because parts of an if-statement may be a complete program statement that abides by the rules governing program states. The following definitions capture the basic syntax of the if-statement used on these pages.
The if-statement is a finite sequence of ordered guarded commands inside an if-endif pair. Each guarded command contains a guard and a guarded statement. Each pair is denoted by an integer, so there is a first guarded command and a last guarded command. The denotations represent the order in which the guarded commands are activated.
In contrast to a simple sequence of guarded commands, the if-statement is an alternative construct, and activation of a guarded command in the if-statement depends on the behavior of prior guarded commands in the if-statement. If a guard is true, then, according to the alternate form, subsequent guarded commands are not activated.
Definition 1: IF[k,n] = (if (||i|k£i£n: (B[i]®r[i])) endif)
The || corresponds to the sequence operator for program statements (;). The || operator separates guarded commands in an if-statement. Unlike the sequence operator, the || operator denotes the alternate form of the sequence. The if and endif symbols denote the beginning and end of the alternate form of operation.
An empty if-statement is an empty sequence of guarded commands inside an if-endif pair
Definition 2: if endif = (if (||i|false: (B[i]®r[i])) endif)
A sequence of guarded commands in an if-statement may be written in shorthand notation in a way similar to guarded command sequences. The shorthand notation is useful when combining two guarded command sequences into one if-statement.
Definition 3: I[k,n] = (||i|k£i£n: B[i]®r[i])
I[false] = (||i|false: B[i]®r[i])
The semantic meaning of the if-statement relies on definitiion of a guarded command sequence G[k,n] in which each guarded command in the sequence is guarded by a unique flag variable associated with the sequence.
A unique flag is associated with each if-statement. The scope of the flag
variable is limited exclusively to the if-statement even to the extent that the
flag is not associated with any guarded statement r[i]. If the flag is set to true, then
activation of G[k,n] proceeds until a guard B[i] is true. When the guard
B[i] is true, then the flag is set to false, and subsequent guards will not
activate. A Hoare triple containing an if-statement is equivalent to
setting a flag true, then activating a sequence of guards G[k,n].
Axiom 1: P {IF[k,n]} R º P {flag := true;G[k,n]} R
P {IF[false]} R º P {flag := true;G[false]} R
The theorems that follow will describe an if-statement with a special relationship between all of the guards and the respective guarded statements. When each guarding set is a subset of guarded statement’s weakest precondition, then the if-statement is well-formed with respect to the result set R.
if-statement Theorems
The following theorems describe how to define a Hoare Triple consistent with the if-statement definitions and axioms.
The empty if-statement contains an empty sequence of guards, so the empty if-statement behaves like the skip statement.
Theorem 1: P {if endif} R º P {skip} R
There is a set of solutions to an if-statement corresponding to the set of solutions to the special sequence of guarded commands. A member of the set corresponds to one of the guards in the if-statement.
Theorem 2: ("i|k£i£n:B[i] Í WP.r[i].R) Þ
("j|k£j£n:(B[j] Ç (Çi|k£i£ j-1:~B[i])) {IF[k,n]} R
The set of solutions described in Theorem 8 may be combined by the set-union operator to form a more general solution.
Theorem 3: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
(Èj|k£j£n:B[j]) {IF[k,n]} R
The intersection of the precondition with all the non-guards forms a solution equivalent to the skip statement.
Theorem 4: (P Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R º (P Ç (Çi|k£i£n:~B[i])) {skip} R
Because the intersection of the precondition with all the non-guards forms a solution equivalent to the skip statement, then the invariant properties of the skip statement correspond to the if-statement solution.
Theorem 5: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} (R Ç (Çi|k£i£n:~B[i]))
Corollary: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} R
Corollary: (R Ç (Çi|k£i£n:~B[i])) {IF[k,n]} (Çi|k£i£n:~B[i])
If the intersection of all the non-guards is a subset of the result set, then the intersection of non-guards forms a solution to the if-statement.
Theorem 6: (Çi|k£i£n:~B[i]) Í R Þ
(Çi|k£i£n:~B[i]) {IF[k,n]} R
When an if-statement is well-formed and the intersection of all non-guards is a subset of the result, then any precondition forms a solution.
Theorem 7: ("j|k£j£n:B[j] Í WP.r[j].R) Ù (Çi|k£i£n:~B[i]) Í R Þ
U {IF[k,n]} R
When at least one guard is true, then the result set is an invariant. If the result is already true, it will remain true.
Theorem 8: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
R Ç (Èj|k£j£n:B[j]) {IF[k,n]} R
Theorem 9: ("j|k£j£n:B[j] Í WP.r[j].R) Þ
WP.IF[k,n].R = (Èj|k£j£n:B[j]) È R
A programming problem:
Write an adder program that adds or subtracts argument b from argument a depending on the value of argument c. The program should accept three arguments, two objects that have a ‘value’ property and one string argument. The values of arguments a and b are positive integers, and the value of argument c is ‘+’, ‘-‘, or some other value. If argument c is not ‘+’ or ‘-‘ then no operation should be performed.
The expected result R is
R = (c = ‘+’ Ù a.value = a.value + b.value)
Ú (c = ‘-’ Ù a.value = a.value - b.value)
Ú (c ¹ ‘+’ Ù c ¹ ‘-’ Ù a.value = a.value)
Let B[0] be “c = ‘+’”, and let r[0] be “a.value = a.value + b.value”.
Let B[1] be “c = ‘-’”, and let r[1] be “a.value = a.value - b.value”.
Assume that a.value and b.value are numbers.
It can be shown that
(("i|0£i£1:~B[i]) Í R) Ù ("i|0£i£1:B[i] Í WP.r[i].R).
Thus, activation of the related if-statement will have the expected result R, leading to the following program.
function adder (a, b, c)
Begin
if
c = ‘+’ à a.value := a.value + b.value
|| c = ‘-’ à a.value := a.value - b.value
endif
end
Mapping the if-statement 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.
Guarded commands may be implemented in JavaScript using simple JavaScript if-statements. The guarded command may be implemented with a simple JavaScript if-statement.
(B ®r) º {if (B) r;}
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];}
When a sequence of guarded commands is delimitted by an if/endif pair, then the if-statement definition takes effect. The if-statement may be implemented by introducing a flag variable in a special sequence of guarded commands.
if B[0] ®r[0] || (B[1] ®r[1] endif º
flag = true;
if (flag) if (B[0]) {flag = false; r [0]}
if (flag) if (B[1]) {flag = false; r [1]}
The syntax of the sequence of guarded commands is chosen so that the meaning of the if-statement is the same as the meaning of a JavaScript if-statement using the if-else-if form.
if B[0] ®r[0] || (B[1] ®r[1] endif º
{if (B[0]) r[0]; else if (B[1] r [1];}
The if-statement programming example demonstrates the three JavaScript examples shown above with three executable scriptlets.
The first scriptlet is an example of a sequence of guarded commands. Each JavaScript if-statement represents a guarded command, so the second JavaScript if-statement executes indendent of the first JavaScript if-statement.
The second scriptlet is an example of a sequence of guarded commands that are equivalent to an if-statement. As in the first scriptlet, the second guarded command executes independent of the first guarded command, but activation of the imbedded guarded command is controlled by the flag variable. The final state in the second scriptlet differs from the final state in the first scriptlet.
The third scriptlet is an example of a JavaScript if-statement if if-else-if format that is equivalent to the if-statement represented by the sequence of guarded commands in the second scriptlet.
Please experiment with the scriptlets by modifying them and executing them under different scenarios.
Problems:
Using Assignment Statement Theorem 8, show that each implication in
("i|0£i£1:B[i] Í WP.r[i].R)
is true.
Show that ("i|0£i£1:~B[i]) Í R is true.
In contrast to Part 1 Theorem 2, Theorem 1 shows that the empty if-statement behaves like the skip statement. Explain the apparent contradiction between the two theorems.
The example program shows how to use JavaScript to test out programming problems. Here is one. You must calculate your income tax according to the following rules:
Income Tax rate
$0-15,000 5%
15,001-30,000 10%
30,001-45,000 15%
45,000+ 20%
If your income is $33,000, your taxes are at 5% for the first $15,000, 10% for the next $15,000 and 15% for the last $3000.
Code the if-statement then test it using the example program or one of your own.
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.