Programming Notes – Flag Variable

 

A flag variable is a logical variable that is used in a guard to control activation of a guarded statement based on the conditions of the program state.  A flag variable has two primary uses.  First, a way of expressing an equivalent program statement is by introducing a flag variable.  Second, a flag variable may be used as a way of defining how a sequence of guarded commands acts as one if-statement of a sequence of if-statements acts as one do-statement. 

 

The flag variable has two properties.  First, the flag variable has an arbitrarhy value and should not affect the truth-value of any expected outcome R, nor should it affect the truth-value of any precondition P.

 

Axiom 1: (flag is arbitrary) ØOccurs(flag, Q) (Q may be a precondition or an expected result)

 

A unique flag is associated with each if-statement.  The scope of the flag is limited exclusively to the if-statement even to the extent that the flag is not associated with any guarded statement r.  Thus, activation of any guarded statement does not affect the value of the flag variable.

 

Axiom 2: (scope of flag) WP.r.{x|flag=E} = {x|flag=E}ÇWP.r

 

Theorems

The flag variable’s non-involvement in any related predicate allows for modifying the variable without changing the truth-value of the relevant program state.

 

Theorem 1: Given K is a constant of consistent type for Prog.x Ù

      ØOccurs(Prog.x, P),

      P {x := K} P Ç {State.s|: Prog.x = K} 

 

 

Corollary: Given x is a flag variable, K is a constant of consistent type for Prog.x, P is a precondition or postcondition,

      P {x := K} P Ç {State.s|: Prog.x = K} 

 

Any Hoare Triple implied by the results of Theorem 1 are also theorems.  The precondition can be restricted, for example.

 

Theorem 2: Given x is a flag variable, K is a constant of consistent type for Prog.x, P Ç Q, P are preconditions or postconditions,

      P Ç Q {x := K} P Ç {State.s|: Prog.x = K} 

 

It also follows that the value of the flag variable can be dropped from the postcondition.

 

Theorem 3: Given x is a flag variable, K is a constant of consistent type for Prog.x, P is a precondition or postcondition,

      P {x := K} P  

 

The program statement that assigns a flag value to a flag variable has an equivalent skip statement form.

 

Theorem 4: Given x is a flag variable, K is a constant of consistent type for Prog.x, R is a precondition or postcondition,

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

 

Assignment of a new value to a flag variable always changes the value to a new value.

 

Theorem 5: Given x is a flag variable, J and K are constants of consistent type for Prog.x,

      {State.s|:x=J} {x := K} {State.s|:x=K}

 

If two flag variables are assigned new values in a sequence, then the two flag variables are changed, but precondtions or postcondtions remain unchanged.

 

Theorem 6: Given x and y are flag variables, J and K are constants of consistent type for Prog.x, Prog.y, respectively, and P is a precondition or postcondition,

       P {x := J; y :=K} P Ç {State.s|:x=K}Ç{State.s|:x=K}

 

The prior theorem can be restated by adding one of the flag variables to the precondition.  Of course, the assignment statement changes the value of the precondition as related to the flag variable. 

 

Theorem 7: Given x and y are flag variables, J and K are constants of consistent type for Prog.x, Prog.y, respectively, and P is a precondition or postcondition,

       P Ç {State.s|:x¹J} {x := J; y :=K} P Ç {State.s|:x=J}Ç{State.s|:y=K}

 

The program statement sequence that assigns values to two flags has an equivalent skip statement form.

 

Theorem 8: Given x, y are flag variables, J, K are constants of consistent type for Prog.x and Prog.y, R is a precondition or postcondition,

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

 

The theorem is still true when the references to the variables are omitted from the expected result.

 

Theorem 9: Given x, y are flag variables, J, K are constants of consistent type for Prog.x and Prog.y, R is a precondition or postcondition,

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

 

 

 

Problems:

Flag variables do not occur in precondtions and postconditions.  Determine which of the following conditions are appropriate.  The variable x used below is a flag variable. 

 

{State.s|: base*height > 100}

{State.s|: base*height > 100 Þ x = false}

 

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.