Programming Notes – Programming Solutions Part 1

 

The goal of a program statement is to achieve some expected result.  A programming solution is that combination of initial state and program statement that achieves the expected result.  Suppose that R is an expected result.  The Hoare Triple 

 

      P {r} R

 

is a programming solution in which the precondition in the Hoare Triple is a subset of the weakest precondition.  Given the initial state P, proper termination of program statement r must lead to expected result R.

 

The process of designing a program is really the process of deriving a sequence of programming solutions, and the most basic process involves the derivation of a programming solution for one programming statement.  This page contains a few simple rules that help to formalize the derivation of programming solutions for a single program statement.

 

Condition of a result

The condition of an expected result is the set of program states that lead to the expected result.  The form of the condition is an extension of set-relations concepts found in Theory of Conditions.  The program statement condition uses the relation corresponding to the program statement, and may be defined as:

 

Definition 1: cond.r.R = dom.r.R – dom.r.~R

 

The domain of R contains all points that map into the set R.  The condition contains the domain points less any points that also map into a point not in R.  The condition of R forms the solution:

 

 

Program Statement Solutions

A program statement solution is any precondition, program statement, and expected result that form a Hoare Triple satisfying the requirements of Weakest Precondition Axiom 2. 

 

Finding a program solution has one of two goals; either to find a proper precondition for a specific expected result and program statement or to find a proper program statement for a specific precondition and expected result.

 

The most obvious solution to a weakest precondition is the weakest precondition.

 

Theorem 1: WP.r.R {r} R

 

The set-condition also forms a solution. 

 

Theorem 2:  cond.r.R {r} R

 

When the relation corresponding to the program statement r is a function, the domain dom.r.R is also a condition cond.r.R.  Therefore the domain of a program statement that behaves like a function is also a solution.

 

Theorem 3: r is a function Þ dom.r.R {r} R

 

If the domain of a result is disjoint from the domain of the result’s complement, then the domain is also a solution.

 

Theorem 4: (dom.r.R Ç dom.r.~R = Æ) Þ dom.r.R {r} R

 

One can derive new solutions from existing solutions by using the properties of WP.r.R.  If result R is a subset of set S, then solutions using result R are also solutions using result S.

 

Theorem 5: R Í S Þ (P {r} R Þ P {r} S)

 

Corollary: (R Í S Ù P {r} R) Þ P {r} S

 

If set P is a subset of precondition Q, then solutions using precondition Q are also solutions using precondition P. 

 

Theorem 6: P Í Q Þ (Q {r} R Þ P {r} R)

 

Corollary: (P Í Q Ù Q {r} R) Þ P {r} R

 

If there are two solutions for a program statement, then there is a solution using the intersection of the preconditions and the intersection of the results. 

 

Theorem 7: P {r} R Ù Q {r} S Þ (PÇQ) {r} (RÇS)

 

If there are two solutions for a program statement, then there is a solution using the union of the preconditions and the union of the results. 

 

Theorem 8: P {r} R Ù Q {r} S Þ (PÈQ) {r} (RÈS)

 

Two program solutions with the same precondition and program statement are together equivalent to a solution containing the intersection of the result sets.

 

Theorem 9: P {r} R Ù P {r} S º P {r} (RÇS)

 

Two program solutions with the same result set and program statement are together equivalent to a solution containing the union of the preconditions.

 

Theorem 10: P {r} R Ù Q {r} R º (PÈQ) {r} R

 

Any subset of the weakest liberal precondition intersected with the termination set is also a solution.

 

Theorem 11: B Í WLP.r.R Þ (B Ç T.r) {r} R

 

The property that two program statements form equivalent Hoare Triples for an expected result and all preconditions is equivalent to the property that the corresponding weakest preconditions are equal.

 

Theorem 12: WP.r.R = WP.s.R º ("B|B r R º B {s} R:B)

 

Corollary: WP.r.R = WP.s.R Þ P {r} R º P {s} R

 

The condition that all corresponding weakest precondions of two program statements are equal is equivalent to the condition that all corresponding Hoare Triples formed by the two program statements are equivalent.

Theorem 13: ("B|WP.r.B = WP.s.B:B) º ("B|("A|A {r} B º A {s} B:A):B)

 

The weakest precondition is a solution, so any subset of the weakest precondition is a solution.  Any intersection with the weakest precondition is also a subset and a solution.

 

Theorem 14: (B Ç WP.r.R) {r} R

 

If two weakest preconditions form solutions with opposite program statements, they are equal to each other.

 

Theorem 15: (P Ç WP.r.R) {s} R Ù (P Ç WP.s.R) {r} R Þ

            P Ç WP.r.R = P Ç WP.s.R

 

The null set forms a solution with any program statement and final result.  All valid program states lead to a solution, and no valid program state leads to abnormal termination.  The solution is not very interesting because there is no valid program state to form a solution.  That is, the solution set is null.

 

Theorem 16: Æ {r} R

 

Suppose that S is a precondition of program statement r.  Then any solution formed by a subset of S is equivalent to the combined solutions.  A corollary involves the universal set in an interesting way.  If a program statement always leads to a result, then the result may be added to any other solution involving the program statement.

 

Theorem 17: (P Í S Ù S {r} Q) Þ (P {r} R º P {r} (RÇQ))

 

Corollary: (U {r} Q) Þ (P {r} R º P {r} (RÇQ))

 

What happens if a state space leads to a Hoare Triple with an empty result set?  No valid program state will terminate normally and not have a valid result state, so the condition set must also be empty.

 

Theorem 18: P = Æ º P {r} Æ

 

If two solutions have complementary results, then the common precondition must be empty.

 

Theorem 19: P {r} Q Ù P {r} ~Q º P = Æ

 

Hoare Triple as an exptession

There is a set of ordered pairs corresponding to a Hoare Triple the Hoare Triple P {r} R:

 

      {p,r|{p} {r} {r} Ù pÎP Ù rÎR:<p,r>}

 

There is a temptation to evaluate the validity of the Hoare Triple based on the content of the set of ordered pairs, but the set-based validation of the Hoare Triple us not satisfactory.  The following two examples illustrate the basic weakness of basing Hoare Triple validity purely on the set of ordered pairs.

 

The first example deals with a special case of Theorem 16, above; the empty solution.

 

      Æ {r} Æ                     (1)

 

The set of ordered pairs corresponding with expression (1) is empty, and true for any program statement.

 

Suppose P ¹Æ that forms the Hoare Triple

 

      P {r} Æ                       (2)

 

The set of ordered pairs corresponding to expression (2) is also empty, but, according to Theorem 18, expression (2) is false.

 

The corresponding set of ordered pairs for each expression is the empty set; but the first Hoare Triple is true, and the second Hoare Triple is false.

 

The second example deals with an empty set combined with a valid solution.  Suppose that the Hoare Triple

 

      P {y := y/x} R                (3)

 

is true.

 

The Hoare Triple

 

      {s|x=0:s} {y := y/x} R        (4)

 

is false, because program statement fails with the precondition {s|x=0:s}.  The set of ordered pairs corresponding to expression (4) is empty.

 

the Hoare Triple formed by the union of experssions (3) and (4)

 

       P È {s|x=0:s} {y := y/x} R   (5)

 

is false, according to Theorem 10, but the set of ordered pairs corresponding to expression (5) equals the set of ordered pairs corresponding to expression (3).  Again, two distinct Hoare Triples correspond to the same set of ordered pairs.

 

The set-relation property of a Hoare Triple does not convey enough information for analyzing a program statement, and the Hoare Triple is much more effective when it is simply an expression.

 

 

Program Example

Bob Stanton’s clever Maze Problem as shown in Games Magazine provides an excellent opportunity to discover program statement solutions using a program statement very different from statements common to conventional programming languages.

 

The Maze Problem game consists of a square configuration of 36 cells plus an entry cell in the upper left-hand corner and an exit cell in the lower right-hand corner.  The purpose of the game is to move the cell marker from the entry cell to the exit cell according to the rules of the game.  The cell marker may move to any cell in the direction indicated by the marked cell.  The direction of movement for the next move depends on the direction indicated by the target cell.  The cell marker continues through the maze until it reaches the exit cell.

 

Activation of a Maze Problem program statement moves the cell marker the number of cells indicated by the instruction in the direction indicated by the cell.  For example, a first move of 3 moves the cell marker down 3 cells.  If the number of cells is greater than the available cells in the indicated direction, then the cell marker stops at the end of the row or column.

 

Each cell may be denoted by the row and column of the cell starting with row 0 and column 0.  The starting cell in the upper left hand corner is cell(0,0).  The bottom cell in the first column with an ‘R’ direction is cell(6,0), because the cell is in row 6 and column 0.  The exit cell in the bottom right corner is in row 7 and column 5 and denoted by cell(7,5).

 

Suppose the first move is move(1).  Then the cell marker would move down 1 cell to cell(1,0).  The direction of cell(1,0) is R for right.  A second move of move(3) sends the cell marker to cell(1,3).

 

There is only one result for any move in the Maze Problem game, so the relation for each move is a function.  Theorem 3, above, shows that a solution to a program statement and expected result is the domain.  Suppose that the target cell is cell(1,3) and the move is move(3).  The domain contains any cell that is 3 cells away in the same row or column with a direction towards cell(1,3).  Thus

 

      dom.move(3),{cell(1,3)} = {cell(1,0),cell(4,3)}.

 

 

 

 

Problems:

1. Play the Maze Problem until you are familiar with the program.

2. dom.move(1).{cell(7,5)} = Æ.  Why?

3. What cell or cells could lead to a move to cell(7,5)?  What would be the move, and how would the domain be stated?

4. What cell or cells could lead to the domain of cell(7,5)?  What would be the move, and how would the domain be stated?

 

 

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