Programming Notes – skip Statement

 

skip Statement

The skip statement does not change the program state, so it does not, by itself, move the program closer to the expected result.  The skip statement provides a syntactic placeholder in a program statement.  If-statements and while-statements are control statements that contain other statements.  The following if-statement sets variable x to expression E when condition B is true.

 

      if B à x := E endif

 

The following if-statement also sets variable x to expression F when condition C is true.

 

      if

         B à x := E || C à x := F

      endif

     

Suppose that the if-statement must be changed further so that no action occurs when condition B is true.  The skip statement satisfies the requirement without violating the syntactic rules of the programming language grammer.  Thus

 

      if

         B à skip || C à x := F

      endif

 

is a syntactically correct if-statement that clearly expresses the intended result.

 

Using Dijkstra’s weakest precondition form, the semantics of the skip statement is

 

      WP(skip,R) = R

 

The set relation model asserts a property of each member of the relation associated with the skip statement.  That is, the initial state is the same as the result state.

 

Axiom 1: a skip b º a = b

 

The properties of the skip relation are similar to the properties of the identity relation described in Identity Relations.

 

An interesting property of the skip relation is the value of a domain; the domain of the skip relation equals the result.

 

Theorem 1: dom.skip.R = R

 

The cond of a result may be derived directly from the value of the domain.

 

Theorem 2: cond.skip.R = R

 

The Hoare Triple solution relies on Theorem 2 and the simplicity of the skip statement.

 

Theorem 3: R {skip} R

 

The result set R is also the weakest precondition.

 

Theorem 4: WP.skip.R = R

 

The skip statement serves as the left and right identity with respect to the sequence operation.  As such, the skip statement is the identity statement with respect to the sequence operation.

 

Theorem 5: (Left Identity) WP.(skip;r).R = WP.r.R

 

Corollary: P {skip;r} R º P {r} R

 

Theorem 6: (Right Identity) WP.(r;skip).R = WP.r.R

 

Corollary: P {r;skip} R º P {r} R

 

The skip statement can come in many forms.  If a variable is assigned a constant,and the variable is not used in a resulting condition, then activating the assignment statement is equivalent to activating the skip statement relative to the expected result.

 

Theorem 7: Given K is a properly typed constant Ù Øoccurs(x,R),

P {x := K} (RÇ{State.s|:x=K}) º P {skip} R

 

The previous theorem can be generalized to omit the reference to the assigned variable in the expected result.

 

Theorem 8: Given K is a properly typed constant Ù Øoccurs(x,R),

P {x := K} R º P {skip} R

 

If a statement is equivalent to the skip statement, then the statement can be omitted from the back side of a sequence.

 

Theorem 9: P {r} WP.s.R º P {skip} WP.s.R º P {r;s} R º P {s} R 

 

Similarly, if a statements weakest precondition equals the weakest precondition of the skip statement, then the statement can be omitted from the front side of a sequence.

 

Theorem 10: WP.s.R = WP.skip.R Þ P {r;s} R º P {r} R

 

If two assigned variables do are not part of a result, then sequentially assigning values to the variables does not affect the result.  Thus, assigning values to unrelated variables is equivalent to applying the skip statement.

 

Theorem 11: Given J,K is a properly typed constants Ù Øoccurs(x,R) Ù Øoccurs(y,R),

P {x := J;y :=K} (RÇ{State.s|:x=J} Ç{State.s|:y=K}) º P {skip} R

 

The previous theorem can be generalized by omitting any references to the two assigned variables in the expected results.

 

Theorem 12: Given J,K is a properly typed constants Ù Øoccurs(x,R) Ù Øoccurs(y,R),

P {x := J;y :=K} R º P {skip} R

 

Just as the domain equals the result, the range of the skip statement equals the precondition.

 

Theorem 13: ran.skip.P = P

 

It follows that the Strongest Result of the skip statement equals the range of the precondtion

 

Theorem 14: SR.skip.P = P

 

  

Summary

The skip statement may be used as a placeholder, and the skip statement is valuable in the analysis of other program statements.

 

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