Programs

[ //csci.csusb.edu/dick/maths/math_76_Concurency.html ]

[ //csci.csusb.edu/dick/maths/math_73_Process_algebra.html ]

Correctness

Liveness and Performance

The Laws of Programming

This presents an algebraic set of "Laws of Programming"(LAW1 & LAW2).

An alternative set of laws is developed by [ Maddux96 ] , see RELATION_ALGEBRAS.

Basis

The paper works with the following terms:
1. Programs::Sets. Elements in an algebra that abstracts the ways that programs can be constructed.
2. ABORT::Programs=a program that has totally unpredicatable results.
3. Id::Programs=the program that has no effect. (;) ::infix(Programs). Sequential combination of two programs to give a new program. (|) ::infix(Programs). Nondeterministic choice.
4. BOOLEAN( Boolean_expressions, and, or, not, true, false). (*) ::infix(Boolean_expressions, Program, Programs).
5. For each Boolean_expression b, (<|b|>) ::infix(Programs). The original paper (LAW1) remarks that the following mapping into the calculus of relations is inconsistent with the laws proposed.
6. Rel1::=following
   Net
   1. States::Sets. The set of possible states that the program can be in.
   2. Programs::@(States, States). Programs=set{P. for all s:States( s.P in non_empty &(Finite | {States}}. ABORT= States><States.

      S3 below requires ABORT;P=ABORT for all P. If we choose P to be the relation that maps any state in state s then img(ABORT;P)={s} but img(ABORT)=States. So if States has more than two elements ABORT;P can not always be the same as ABORT. Indeed the image of ABORT;P` is nearly always less than P.

      Mathematically in any semigroup only one element can be an anihilator or zero. So the S3 implies that ABORT is unique. Now if one includes the null program - which fails or fails to terminate in all states then this is an anihilator, and so the unique zero. If one omits this for the set of programs then no other program can take its place. Thus S3 is not consistent with the statement in LAW1 that programs are total relations with finite or universal images.

      Worse D4:(ABORT|P)=ABORT follows from the definition of ABORT=States><States.

      The stated requirement for totallity does not fit with the observed behavior of a program like true*skip that can have no successor state.

      Further the axioms in LAW1 do not define a complete Boolean Algebra. They do not define (or need) the complement operation. This makes sense because complements of intuitive program statements are highly unintuitive. For example the complete of an assignment 'x:=1' is an "operation" that can change the state of the system in any way, as long as x is not equal to 1 afterwards. In the absence of a Boolean Algebra we do not have any kind of Relation Algebra.

   
   (End of Net)
   
   

   Model as total relations

   Given these worries this model will be abandonned. A technical report from Oxford University develops an alternative theory for the given LAWS.
7. States::Sets. The set of possible states that the program can be in.
8. Non_terminating::State. A state at infinity.

9. Programs::={R:@(States, States). R in Total. R in finite_or_arbortive. R in non_terminating_aborts}.
10. Total::={R. for all x, some y, x R y}.
11. finite_or_abortive::={R. for all x( x.R in Finite or x.R=States}.
12. non_terminating_aborts::={R. for all x( if x R Non_terminating then x.R=States}.

13. ABORT::Programs= States><States.
    
14. (Programs, Total)|-{} in @(States, States)~Programs. The ABORT program is, as LAW1 states the worst program possible - anyhting can happen.

    Basic Structures

15. (seq): For Programs P,Q, (P;Q) in Programs.
16. (union): P|Q in Programs.

17. Boolean_Expressions::@States.
18. For Boolean_expressions b, Programs P,Q, P<|b|>Q::= b;P | no b;Q.

19. For Boolean_Expressions b,c,d, b<|c|>d:: Boolean_Expressions = if c then b else d.

20. For b,P, b * P::@(States,States)= while(b)(P).

    
    (while): (b*P)=P;(b*P)<|b|>Id.

    A Problem

    Parnas notes another problem in that it is impossible to distinguish between and infinite loop and a program that fails in a finite time.

    Parnas's solution is define for a program text a set of states in which it is known that the program text terminates. This does not have to be the largest set of states... just those which termination can be shown to occur. A requirement is then a combination of a set of states in which termination occurs and a program.

    This is particularly confusing with program texts that apparently mean things like this: (true*P)|Q.

    Is this angelic where the set of safe states is those of Q, or demonic where the set of safe states is empty?

    Maddux [Maddux96] has demonstrated how programs can be modelled as a pair of relations. The first indicates states in which the program fails to terminate. The second indicates what happens in thoise states that do terminate.

    . . . . . . . . . ( end of section A Problem) <<Contents | End>>

21. For F:Programs->Programs, X:Variable, μ(X. F(X)) ::= F(μ(X. F(X)). The original paper(LAW1) establishes that an equation like this does define a solution using Dana Scott's CPO model of limits.

    
    (recwile): b*P= μ(X. (P; X)<|b|>Id.

    Variables and Expressions

22. Variables::Sets.
23. Expressions::Sets.
24. Values::Sets.
25. For States s, Variables v, v(s) ::Values.
26. For States s, Expressions e, e(s) ::Values.
    
27. |-Variables ==> Expressions.

28. List_of_Variables::= Variables^(1..) and Distinct.
29. Distinct::=set_of{V. for all i,j:1..|V| ( if V(i)=V(j) then i=j)
30. List_of_Expressions::=Expressions^(1..).

    |-For List_of_Variables V, List_of_Expressions E, if |V| = |E| then (V:=E) :: Programs.

    |-(as1): For V:List_of_Variables, i:1..|V|, E::(Expresssions^|V|), v:=V(i), e:=E(i), s,s':States, if s(V:=E)s' then v(s)=e(s). |- (as2): For V:List_of_Variables, E::(Expresssions^|V|), v:=Variable~img(V), s,s':States, if s(V:=E)s' then v(s)=v(s).

    Laws

31. For P,Q,R:Programs.
32. For b,c,d:Boolean_expressions.
33. For e,f,g:Expressions.
34. For E,F,G:Lists_of_Expressions.
35. For x,y,z:Lists_of_Variables.

    Two Program are said to be equal if they have the same meaning. Two program texts may differ but still have the same meaning. Two program texts that have the same effect but take different times are taken to be equal programs.

    Nondeterministic Choice

    
    
36. |- (ndsym): P|Q = Q|P.
    
37. |- (ndass): P|(Q|R)=(P|Q)|R.
    
38. |- (ndidp): P|P = P.
    
39. |- (ndz): ABORT | P = ABORT. ndz is consistent with the informal arguments that ABORT is the ultimately bad program that must be avoided. It is also consistent with the theoretical model described above.

    
    

40. |-| in serial(Programs).

    Conditionals

    
    
41. |- (c1): P<|true|>Q = P.
    
42. |- (c2): P<|false|>Q = Q.

    Since c1 and c2 hold for all P and Q it follows that:
    

43. (c1)|- (c1a): P<|true|>ABORT = P.
    
44. (c2)|- (c2a): ABORT<|false|>Q = Q.

    
    

45. |- (c3): P<|b|>P = P.
    
46. |- (c4): P<|b|>(Q<|b|>R) = (P<|b|>Q)<|b|>R. This can be strengthened to
    
47. |- (c4a): P<|b|>(Q<|b|>R) = (P<|b|>Q)<|b|>R = P<|b|>Q.

48. (c5): P<|b|>Q = Q<|not b|>P.
49. (c6): P<|c<|b|>d|>Q = (P<|c|>Q)<|b|>(P<|d|>Q).
50. (c7): P<|b|>(Q <|b|>R) = P<|b|>R.
51. (c8): (P|Q)<|b|>R = (P<|b|>R)|(Q<|b|>R).
    
52. (c5)|- (c9): R <|b|>(P|Q) = (R<|b|>P)|(R<|b|>Q).
53. (c10): (P<|b|>Q)|R = (P|R)<|b|>(Q|R).
54. (c11): (P<|b|>Q)<|c|>R = (P<|c|>R)<|b|>(Q<|c|>R).
    
55. (c1, .., c11)|- (c12): (P<|c|>R)<|b|>(Q<|d|>R) = (P<|b|>Q)<|c<|b|>d|>R.

    Sequences

    
    
56. |- (s1): P;(Q;R)=(P;Q);R.
    
57. |- (s2): Id;P = P;Id = P.
    
58. |- (s3): ABORT;P = P; ABORT = ABORT. This works fits the model because P is a total relation.
    
59. |- (s4a): (P|Q);R = (P;R) | (Q;R).
    
60. |- (s4b): R;(P|Q) = (P;R) | (R;R).
    
61. |- (s5): (P <|b|>Q);R = (P;R)<|b|>(Q;R).

    Assignment

    
    
62. |- (a1): (x:=E; x:=F(x)) =(x:=F(E)).
    
63. |- (a2): (x:=x) = Id.
    
64. |- (a3): (x,y:=E,y) = (x:=E).
    
65. |- (a4): (x,y,z:=E,F,G) = (y,x,z:=F,E,G).
    
66. |- (a5): (x:=E;(P<|b(x)|>Q)=((x:=E;P) <|b(E)|>(x:=E;Q).
    
67. |- (a6): ((x:=E<|b|>(x:=F)) = (x:=(E<|b|>F)).
    
68. |- (a7): (e,E)<|b|>(f,F)=(e<|b|>f), E<|b|>F).
    
69. |- (a8): (x:=E; (x:=F(x)<|b(x)|>x:=G(x))) = (x:=( F(E)<|b|>G(E) )).
    
70. (a1, a2, a3, a5, a6)|- (a9): ((x:=E<|b|>ABORT); (x:=F(x)<|c(x)|>ABORT)) = (x:=F(E)<|c(E)<|b|>false|>ABORT).

    Undefined Expressions

71. D::=Domain_of_definition.
72. \swash_D::=D.
73. For Expressions e, Domain_of_definition(e)::Boolean_expression=`true if the evaluation of e would succeed and false otherwise`
74. For List_of_Expressions E, Domain_of_definition(E)::Boolean_expression=true if the evaluation of E would succeed and false otherwise
    
75. |- (d01): D(true)=D(false)=true.
    
76. |- (d02): D(D(E))=true.
    
77. |- (d03): D(E+F)=D(E) and D(F).
    
78. |- (d04): D(E/F)=D(E) and D(F) and F<>0.
    
79. |- (d05): D(E<|b|>F) = D(b) and (D(E)<|b|>D(F).

    Note. Parnas argues that this approach has both theoretical and practical problems. His interest is in ways to annotate existing and developing code to verify its correctness versus a specification. The specifications are based on predicates. He advocates a way to make sure that annotations and specs are well defined even when subexpressions are not defined [Parnas 93] He proposes that certain predicates are chosen to be primitive - returning false if any of their arguments are false. Other predicates are defined in terms of the primitive ones. Thus all predicates are well defined.

    
    

80. |- (d1): ( x:=E = (x:=E<|D(E)|>ABORT)).
    
81. |- (d2): (P<|b|>Q = (P<|b|>Q) <|D(b)|>ABORT).
    
82. |- (d3): ( P<|b|>ABORT = P<|b<|D(b)|>false|>ABORT).
    
83. |- (d4): (P<|b|>P = P<|D(b)|>ABORT.
    
84. |- (d5): ( (P<|b|>Q)<|c|>R = ((P<|c|>R)<|b|>(Q <|c|>R))<|D(b)|>(ABORT<|c|>R).

    
    

85. |- (d6): ((x:=E; x:=F(x)) = (x:=(F(E)<|D(E)|>ABORT) ).
    
86. |- (d7): ( (x:=E;(x:=G(x)<|b(x)|>x:=G(x))) = ( x:=(F(E)<|b(E)|>G(E)<|D(E)|>ABORT) ).

    Dijkstra's Linear search theorem is easily expressed using the partial and unimplementable min function:
    

87. |- (d8): ( i:=0; (not b(i) *(i:=i+1)))= (i:=min{i. b(i) and i>=0}).

    Normal Form

    The original paper proceeds to show that sequence can always be replaced in a program. Each non-iterative or recursive piece becomes a conditional that aborts or permits the selection of an assignment. In other words any program text without iteration or recursion can be reduced to a simple form:
88. |[i](x:=E(i))<|b|>ABORT where the b implies that all the E's are defined. This result is common to several logical formulations of programs including Trace Tables, the calculus of relations, and Parnas's work.

    Programs as a Domain

    Ordering

    1. Q better P::=(P|Q=P).
    2. P worse Q::=Q better P.
       
    3. |-POSET(Programs, better).
       
    4. |- (p4): for all P(ABORT worse P).

       Programs are a poset with a bottom element.

       
       

    5. |- (p5): ((P|Q)worse P) and ((Q|P)worse Q).
       
    6. |- (p6): (R worse (P|Q)) iff (R worse P) and (R worse Q).
       
    7. |- (p7): (|) and (;) and (<|b|>) and (*) in monotonic(worse).

       P|Q is the best program worse then both P or Q.

       
       

    8. (p4, p7)|- (p8): For all P,Q, Q;ABORT worse Q;P and ABORT;Q worse P;Q .

       least upper bounds

       The worst program better than a set of programs. Don't normally exist.
    9. P compatible Q::= some lub[worse]{P,Q}.
    10. P lub Q::=the lub[worse](P,Q).
        
    11. |- (l1): (P worse R) and (Q worse R) iff (P lub Q) worse R.
        
    12. |-P worse (P lub Q) and Q worse (P lub Q).
        
    13. |- (l2): P lub P = P.
        
    14. |- (l3): P lub Q = Q lub P.
        
    15. |- (l4): P lub(Q lub R) = (P lub Q) lub R.
        
    16. |- (l5): ABORT lub P =P.
        
    17. |-SERIAL(Programs, lub).

        
        

    18. |- (l6): if for all P:S(P worse R) then lub(S)worse R.

        Limits

    19. directed::@Programs={ S. some S and for all P,Q:S, some R:S ( P worse R and Q worse R)}.

        ??cf Bourbaki filter?? [click here if you can fill this hole]

        
        

    20. |-For S in Finite&directed( lub(S) in S ).

    21. continuous::Programs->Program= {F. for all directed S( lub(F(S)) = F(lub(s)).

        Since, for infix op, (_op a) = fun[x]( x op a).
        

    22. |- (l1): (_|Q) in continuous.
        
    23. |- (l2): (_ <|b|>Q) in continuous.
        
    24. |- (l3): (_;Q) in continuous.
        
    25. |- (l4): (Q;_) in continuous.
        
    26. |- (l5): (b*_) in continuous.
        
    27. |- (l6): any finite construction using these operators is therefore continuous.

        Iteration and Recursion

        In LAW1 a sequence Q[i:0..] is generated with Q[0]=ABORT and Q[i+1]=(P;Q[i]<|b|>Id). In my model the Kleene sequence is used in its place:

    28. KLEENE::=Net{ P:Programs. b:Boolean_expression. Q:Nat0->Programs. Q[0]=ABORT. Q[i+1]=( (P;Q[i])<|b|>Id ).}.

        Such sequences defined a directed set {Q[i]. i:0..}. and so
        

    29. |- (ir1): b*Q = lub{Q[i]. i:0..}.

        Again if F is an finite construction that makes F(X):Programs out of X there is a Kleene sequence ABORT, F(ABORT), F(F(ABORT)), ... that defines a directed set so that
        

    30. |- (ir2): μ{ X. F(X)} = lub{F^i(ABORT). i:0..}.
        
    31. |- (ir3): b*P= μ{X. P;X<|b|>Id.

        Hence the fixed point law:
        

    32. |- (ir4): μ{X. F(X)} = F(μ{X. F(X)}.

        
        

    33. |- (ir5): if Y=F(Y) then μ{X. F(X)} worse Y.

    . . . . . . . . . ( end of section Programs as a Domain) <<Contents | End>>

    Specifications

    Mili Mile and Abowd argue that a relation is a specification ratherthan a program. In LAW1 a specification is a Program that may not have an implementation. The worse relationship holds between a specification and a satisfactory program. They postulate the existence of a →p Specification that has no satisfactory program. The lub and union operators on sets of specifications are interpretted as specifications requiring, respectively all or some of the subspecifications are satisfied.
    

89. |- (sp1): Q=|(S) iff for all R:S(Q worse R).
    
90. |- (sp2): lub(S)=Q iff for all R:S( R worse Q).

    Weakest Prespecification

    As an aid to top-down design for two specifiations S and A, S\\A is defined as the weakest specification B such that if R satisfies B then R;S satisfies W.

    
    

91. |- (wp1): W worse (S\\W);S
    
92. |- (wp2): W worse (X;S) iff (S\\W) worse X.
    
93. |- (wp3): P\\ →p = →p. No ammount of programming helps you accomplish the impossible.
    
94. |- (wp4): P\\(R1 lub R2) = (P\\R1) lub (P\\R2).
    
95. |- (wp4a): P\\lub(S)=lub{P\\R. R:S}
    
96. |- (wp5): For R:0..->Specifications, if for all i:0..(R(i+1)worse R(i)) then P\\lub img R = lub {P\\R(i). i:0..}.
    
97. |- (wp6): Id\\R = R.
    
98. |- (wp7): m(P|Q)\\R=(P\\R)lub(Q\R).
    
99. |- (wp8): (P;Q)\\R = P\\(Q\\R).
    
100. |- (wp9): (P<|b|>Q)\\R = (P\\R) <[b]>(Q\\R). P<[b]>Q::=if b is true aqfter execution the it behaved P else it behaved like Q.

     PostSpecification and General Inverse

     R//S::=weakest specification of program X such that R worse (S;X).

     
     

101. |- (gi1): R worse S;(R//S).
     
102. |- (gi2): R worse (S;X) iff (R//S)worse X.
     
103. |- (gi3): →p //P=→p.
     
104. |- (gi4): (R1 & R2)//P = (R1//P)&(R2//P).
     
105. |- (gi5): R//Id = R.
     
106. |- (gi6): R//(P|Q)=(P//P)&(R//Q).
     
107. |- (gi7): R//(P;Q)=(R//P)//Q.

     
     

108. |- (gi8): For F:distributes through arbitrary unions,
109. F^-1(R)::=|{P. R worse F(P)}.
     
110. |- (gi9): R worse F(F^-1(R)).

     ??Kelly-Bootle Kludge Theory? [click here if you can fill this hole]

     
     

111. |- (gi10): R worse F(X) iff F^-1(R) worse X.
112. (gi_counter_example):
     Let
     F(X):=X;X, P=(x:=x), Q=(x:=-x).
     
     1. |-P;P=P=Q;Q. P;Q=Q;P=Q.
        
     2. |-F(P|Q)=(P|Q);(P|Q) = P|Q.
        
     3. |-F(P)|F(Q)=P;P|Q;Q=P. ... No F^-1.
     
     (Close Let )
     

     Glossary

113. POSET::= See http://csci.csusb.edu/dick/maths/math_21_Order.html

     min{i:Nat0. p(i)}::=the(i:Nat0. p(i) and for no j<i(p(j))). The first natural number to satisfy p(i). This is not defined when no p.

114. Nat0::=natural numbers plus zero.
115. infix(X)::infix(X,X,X). The set of operators that combine two X's to generate a new X. Written with the operator between the operands.
116. infix(A,B,C)::A><B>->C. The set of operators which when placed between an expression of type A and type B construct an expression of type C.
117. semigroup::= algebra with o:associative(Set). [ math_32_Semigroups.html ]

118. anihilator::=zero.
119. algebra::= logical_system with set:Sets.
120. For semigroup S, zeroes(S)::=set{z:S.Set. for all x( z S.op x = x S.op z = z)}.
121. zero::=singular of zeroes.
122. set(v:S. C)::=set of all x in S that make C true. set{v:S. C}::=set of all x in S that make C true.
123. relations::=sets of pairs of elements. See REL.
124. REL::= See http://csci.csusb.edu/dick/maths/logic_13_relations.html. The set of all binary relations on a given set is a special kind of RELATION_ALGEBRA.

125. RELATION_ALGEBRAS::=plural of RELATIONA_ALGEBRA
126. RELATION_ALGEBRA::= See http://csci.csusb.edu/dick/maths/math_45_Three_Operators.html#RELATION_ALGEBRA.

     pre(R)=set{x. for some y(x R y)}. The pre-condition for R to have a terminal state. See REL. post(R)=set{y. for some x(x R y)}. The postcondition of R. See REL. img(R)=post(R). See REL.

127. x.R::=R(x) ::=set{y. x R y}, states possible after R in state x. See REL. x./R::= /R(x) ::=set{x. x R y}, states leading to state x by R. See REL.

128. serial::=operators where brackets can be omitted and which act on finite lists and sets. Ser SERIAL.
129. SERIAL::= See http://csci.csusb.edu/dick/maths/notn_12_Expressions.html#SERIAL

     References

130. LAWS::=following
     • LAW0::= [Hoare et al 69]
     • LAW1::= [Hoare et al 87]
     • LAW2::= [Hoare et al 87b]
     Comm ACM september 87

131. Maddux96::=following
     [Maddux96] [ RELATION_ALGEBRA ]

     Proofs

     Proof of c4

     1. P<|b|>(Q<|b|>R)
     2. =
     3. b;P | no b;(b;Q|no b;R)
     4. =
     5. b;P | no b;b;Q | no b;no b;R
     6. =
     7. b;P | no b; R.
     8. (P<|b|>Q)<|b|>R
     9. =
     10. b;b;P | b;no b;Q | no b;R
     11. =
     12. b;P | no b;R
     13. =
     14. P<|b|>(Q <|b|> R).

     . . . . . . . . . ( end of section Proofs) <<Contents | End>>

. . . . . . . . . ( end of section Laws of Programming) <<Contents | End>>

Notes on MATHS Notation

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see