.Open Programs
.Road_works_ahead
. Introduction
This sections presents alternate models of computation. One is to develop an explicit model of a random access memory(RAM), expresssions, and control structures. An alternative is to the use the dynamic predicates and the calculus of relations presented elsewhere in MATHS.
.See ./math_14_Dynamics.html
The classical theoretical models - automata, Turing Machines, Markov algorithms are also covered elsewhere.
.See ./math_71_Auto...Systems.html
.See ./math_62_Strings.html
. RAM Modeled by Maps
It is possible to develop a model of computation by modifying what we have presented so far to make an explicit model of random access memory, expresssions, and control structures. This is an alternative to the use of dynamic predicates and the calculus of relations presented elsewhere in MATHS.
RAM::=Net{
The (:=) changes a single value in a map:
|- for A,B, a:A, b:B, f:A->B, (a:=b)(f) = f.(a:=b) = f~(a+>f(a))|(a+>b).
This can be taken further when A and B do not overlap so that (v:=e) is a
well defined operator on a map from A to B whenever v:A and e is an
expression that has elements of both A and B in it. The meaning is that
where-ever an element of B occurs in e it is replaced by the value
currently assigned to it in f.
For example:
.Set
(a+>1, b+>2, c+>3).(a:=2*b+c) = (a+>1, b+>2, c+>3).(a:=2*2+3) = (a+>7, b+>2, c+>3).
.Close.Set
Addresses::Sets.
Values::Sets,
Addresses & Values={}.
Address in denumerable,
Expressions::Sets,
Addresses and Values ==>Expressions,
T,F:Values.
Stores::=Addresses->Values.
Operations::=Stores->Stores.
value::Expressions>Values=map[e,f]`replace each Address v in e by its Value f(v) and simplify`.
For e:Expressions, f:Stores, value(e,f) = substitute( f, e).
Defining the 'substitute' operation is non-trivial....
.See ./notn_12_expressions.html#substitute.
For f:Stores, v:addresses, e:Expressions, f.(v:=e) ::Stores=f~(v+>f(v))|(v+>value(e,f)).
()|- For v:addresses, e:Expressions, (v:=e) in Operations.
|- For v:Addresses, f: Stores, value(v,f) = f(v).
|- For v:Values, f: Stores, value(v,f) = v.
|- For v:Addresses, f: Stores, g:Value->Values, value(g(v),f) = g(f(v)).
|- For v1,v2:Addresses, f: Stores, g:Value^2->Values, value(g(v1,v2),f) = g(f(v1), f(v2)).
|- For n:3.., v:Addresses^n, f: Stores, g:Value^n->Values, value(g(v),f) = g(f(v)).
For each Address `v` in an expression `e`, all occurrences of `v` are removed and replaced by `f(v)`. Because the values and addresses do not overlap the actual order in which this is done does not effect the result.
|- For n:0.., v:Addresses^n, f: Stores, g:Value^n->Values, value(g o v, f) = g o f o v.
A_tempting_formula::=Net{
It is tempting to avoid defining what an expression is and then explicitly defining how two evaluate all the different parts by writing:
value::=map[e,f]( ;[v:Addresses]( f(v).map[v](e) ).
But (1) the `v` in `[v:Addresses]` is different variable to the
second one (in `map[v]`), and (2) there is a unusual use of ';' above which
preseumes that Addresses can be put in sequence and each substitution is
applied to e in that order.
}=::A_tempting_formula.
A better formulation (mathematically speaking) is that `fun[e](value(e,f)`
always defines a homomorphism between expressions and values that preserves
all the operations used in the expressions.
For a,b:Operations, p:Expressions, f:Stores, if value(p,f)=T, f.(if p then a else b fi) ::= f.a.
For a,b:Operations, p:Expressions, f:Stores, if value(p,f)=F, f.(if p then a else b fi) ::= f.b.
For a:Operations, p:Expressions, f:Stores, if value(p,f)=T, f.(while p do a od) ::= f.a.(while p do a od).
For a,b:Operations, p:Expressions, f:Stores, if value(p,f)=F, f.(while p do a od) ::= f.
}=::RAM.
. Structured
.Hole
. Guarded Commands
.Hole
. Sequential
.Hole
. Non-sequential
.See ./math_14_Dynamics.html
.See ./math_76_Concurency.html
.See ./math_73_Process_algebra.html
. Correctness
.Hole
. Completeness.
By Murphy's Law, The only proof of completeness of a specification of a
program is to show that the data specified as input is equal to the set of
all possible inputs with no constraints. Therefore the specification
needs to describe all the possible input sequences and the expected responses.
This means that Data Directed Designs can be shown to be complete.
. Liveness and Performance
.Hole
.Open The Laws of Programming
This presents an algebraic set of "Laws of Programming"($LAW1 & $LAW2).
An alternative set of laws is developed by
.See Maddux96
, see $RELATION_ALGEBRAS.
. Basis
The paper works with the following terms:
Programs::Sets. Elements in an algebra that abstracts the ways that programs can be constructed.
ABORT::Programs=`a program that has totally unpredicatable results`.
Id::Programs=`the program that has no effect`.
(;) ::$infix(Programs). Sequential combination of two programs to give a new program.
(|) ::$infix(Programs). Nondeterministic choice.
$BOOLEAN( Boolean_expressions, and, or, not, true, false).
(*) ::$infix(Boolean_expressions, Program, Programs).
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.
Rel1::=following
.Net
States::Sets. The set of possible states that the program can be in.
Programs::@(States, States).
Programs=$set{P. for all s:States( s.P in non_empty &(Finite_sets(States) | {States}}.
ABORT= States>Q::= b;P | no b;Q.
For Boolean_Expressions b,c,d, b<|c|>d:: Boolean_Expressions = if c then b else d.
For b,P, b * P ::@(States,States)= while(b)(P).
(while): (b*P)=P;(b*P)<|b|>Id.
.Open 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.
.Close A Problem
For F:Programs->Programs, X:Variable, \mu(X. F(X)) ::= F(\mu(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= \mu(X. (P; X)<|b|>Id.
. Variables and Expressions
Variables::Sets.
Expressions::Sets.
Values::Sets.
For States s, Variables v, v(s) ::Values.
For States s, Expressions e, e(s) ::Values.
|-Variables ==> Expressions.
List_of_Variables::= Variables^(1..) and Distinct.
Distinct::=set_of{V. for all i,j:1..|V| ( if V(i)=V(j) then i=j)
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
For P,Q,R:Programs.
For b,c,d:Boolean_expressions.
For e,f,g:Expressions.
For E,F,G:Lists_of_Expressions.
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
|-(ndsym): P|Q = Q|P.
|-(ndass): P|(Q|R)=(P|Q)|R.
|-(ndidp): P|P = P.
|-(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.
|- | in $serial(Programs).
. Conditionals
|-(c1): P<|true|>Q = P.
|-(c2): P<|false|>Q = Q.
Since $c1 and $c2 hold for all P and Q it follows that:
(c1)|- (c1a): P<|true|>ABORT = P.
(c2)|-(c2a): ABORT<|false|>Q = Q.
|-(c3): P<|b|>P = P.
|-(c4): P<|b|>(Q<|b|>R) = (P<|b|>Q)<|b|>R.
This can be strengthened to
|- (c4a):P<|b|>(Q<|b|>R) = (P<|b|>Q)<|b|>R = P<|b|>Q.
(c5): P<|b|>Q = Q<|not b|>P.
(c6): P<|c<|b|>d|>Q = (P<|c|>Q)<|b|>(P<|d|>Q).
(c7): P<|b|>(Q <|b|>R) = P<|b|>R.
(c8): (P|Q)<|b|>R = (P<|b|>R)|(Q<|b|>R).
(c5)|- (c9): R <|b|>(P|Q) = (R<|b|>P)|(R<|b|>Q).
(c10): (P<|b|>Q)|R = (P|R)<|b|>(Q|R).
(c11): (P<|b|>Q)<|c|>R = (P<|c|>R)<|b|>(Q<|c|>R).
(c1,..,c11)|- (c12): (P<|c|>R)<|b|>(Q<|d|>R) = (P<|b|>Q)<|c<|b|>d|>R.
. Sequences
|-(s1): P;(Q;R)=(P;Q);R.
|-(s2): Id;P = P;Id = P.
|-(s3): ABORT;P = P; ABORT = ABORT.
This works fits the model because P is a total relation.
|-(s4a): (P|Q);R = (P;R) | (Q;R).
|-(s4b): R;(P|Q) = (P;R) | (R;R).
|-(s5): (P <|b|>Q);R = (P;R)<|b|>(Q;R).
. Assignment
|-(a1): (x:=E; x:=F(x)) =(x:=F(E)).
|-(a2): (x:=x) = Id.
|-(a3): (x,y:=E,y) = (x:=E).
|-(a4): (x,y,z:=E,F,G) = (y,x,z:=F,E,G).
|-(a5): (x:=E;(P<|b(x)|>Q)=((x:=E;P) <|b(E)|>(x:=E;Q).
|-(a6): ((x:=E<|b|>(x:=F)) = (x:=(E<|b|>F)).
|-(a7): (e,E)<|b|>(f,F)=(e<|b|>f), E<|b|>F).
|-(a8): (x:=E; (x:=F(x)<|b(x)|>x:=G(x))) = (x:=( F(E)<|b|>G(E) )).
(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
D::=Domain_of_definition.
\swash_D::=D.
For Expressions e, Domain_of_definition(e) ::Boolean_expression=`true if the
evaluation of e would succeed and false otherwise`
For List_of_Expressions E, Domain_of_definition(E) ::Boolean_expression=`true if the evaluation of E would succeed and false otherwise`
|-(d01): D(true)=D(false)=true.
|-(d02): D(D(E))=true.
|-(d03): D(E+F)=D(E) and D(F).
|-(d04): D(E/F)=D(E) and D(F) and F<>0.
|-(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
.See [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.
|-(d1):( x:=E = (x:=E<|D(E)|>ABORT)).
|-(d2): (P<|b|>Q = (P<|b|>Q) <|D(b)|>ABORT).
|-(d3): ( P<|b|>ABORT = P<|b<|D(b)|>false|>ABORT).
|-(d4): (P<|b|>P = P<|D(b)|>ABORT.
|-(d5):( (P<|b|>Q)<|c|>R = ((P<|c|>R)<|b|>(Q <|c|>R))<|D(b)|>(ABORT<|c|>R).
|-(d6):((x:=E; x:=F(x)) = (x:=(F(E)<|D(E)|>ABORT) ).
|-(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:
|- (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:
|[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.
.Open Programs as a Domain
. Ordering
Q better P::=(P|Q=P).
P worse Q::=Q better P.
|- $POSET(Programs, better).
|-(p4): for all P(ABORT worse P).
Programs are a poset with a bottom element.
|-(p5):((P|Q)worse P) and ((Q|P)worse Q).
|-(p6):(R worse (P|Q)) iff (R worse P) and (R worse Q).
|-(p7): (|) and (;) and (<|b|>) and (*) in monotonic(worse).
P|Q is the best program worse then both P or Q.
(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.
P compatible Q ::= some lub[worse]{P,Q}.
P lub Q::=the lub[worse](P,Q).
|-(l1):(P worse R) and (Q worse R) iff (P lub Q) worse R.
|-P worse (P lub Q) and Q worse (P lub Q).
|-(l2): P lub P = P.
|-(l3): P lub Q = Q lub P.
|-(l4): P lub(Q lub R) = (P lub Q) lub R.
|-(l5): ABORT lub P =P.
|-$SERIAL(Programs, lub).
|-(l6): if for all P:S(P worse R) then lub(S)worse R.
. Limits
directed::@Programs={ S. some S and for all P,Q:S, some R:S ( P worse R and Q worse R)}.
??cf Bourbaki filter??
.Hole
|-For S in Finite&directed( lub(S) in S ).
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).
|-(l1): (_|Q) in $continuous.
|-(l2): (_ <|b|>Q) in $continuous.
|-(l3): (_;Q) in $continuous.
|-(l4): (Q;_) in $continuous.
|-(l5): (b*_) in $continuous.
|-(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:
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
|- (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
|-(ir2): \mu{ X. F(X)} = lub{F^i(ABORT). i:0..}.
|-(ir3): b*P= \mu{X. P;X<|b|>Id.
Hence the fixed point law:
|-(ir4): \mu{X. F(X)} = F(\mu{X. F(X)}.
|-(ir5): if Y=F(Y) then \mu{X. F(X)} worse Y.
.Close Programs as a Domain
. 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 $top
$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.
top::$Specification.
|- (sp1): Q=|(S) iff for all R:S(Q worse R).
|-(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.
|-(wp1): W worse (S\\W);S
|-(wp2): W worse (X;S) iff (S\\W) worse X.
|-(wp3): P\\ $top = $top. No ammount of programming helps you accomplish the impossible.
|-(wp4): P\\(R1 lub R2) = (P\\R1) lub (P\\R2).
|-(wp4a):P\\lub(S)=lub{P\\R. R:S}
|-(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..}.
|-(wp6): Id\\R = R.
|-(wp7):m(P|Q)\\R=(P\\R)lub(Q\R).
|-(wp8): (P;Q)\\R = P\\(Q\\R).
|-(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).
|-(gi1): R worse S;(R//S).
|-(gi2): R worse (S;X) iff (R//S)worse X.
|-(gi3): $top //P=$top.
|-(gi4): (R1 & R2)//P = (R1//P)&(R2//P).
|-(gi5): R//Id = R.
|-(gi6): R//(P|Q)=(P//P)&(R//Q).
|-(gi7): R//(P;Q)=(R//P)//Q.
|-(gi8): For F:`distributes through arbitrary unions`,
F^-1(R) ::=|{P. R worse F(P)}.
|-(gi9): R worse F(F^-1(R)).
??Kelly-Bootle Kludge Theory?
.Hole
|-(gi10): R worse F(X) iff F^-1(R) worse X.
(gi_counter_example):
.Let
F(X):=X;X, P=(x:=x), Q=(x:=-x).
|- P;P=P=Q;Q. P;Q=Q;P=Q.
|-F(P|Q)=(P|Q);(P|Q) = P|Q.
|-F(P)|F(Q)=P;P|Q;Q=P.
...
No F^-1.
.Close.Let
. Glossary
POSET::=http://www/dick/maths/math_21_Order.html
min{i:Nat0. p(i)}::=the(i:Nat0. p(i) and for no j**->C. The set of operators which when placed between an expression of type A and type B construct an expression of type C.
semigroup::= algebra with o:associative(Set).
.See http://www/dick/maths/math_32_Semigroups.html
anihilator::=$zero.
algebra::= logical_system with set:Sets.
For $semigroup S, zeroes(S) ::=$set{z:S.Set. for all x( z S.op x = x S.op z = z)}.
zero::=singular of $zeroes.
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.
relations::=sets of pairs of elements. See $REL.
REL::=http://www/dick/maths/logic_13_relations.html.
The set of all binary relations on a given set is a
special kind of $RELATION_ALGEBRA.
RELATION_ALGEBRAS::=plural of $RELATIONA_ALGEBRA
RELATION_ALGEBRA::=http://www/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.
x.R::=R(x) .
R(x)::=$set{y. x R y}, states possible after R in state x. See $REL.
x./R::= /R(x),
/R(x) ::=$set{x. x R y}, states leading to state x by R. See $REL.
serial::=operators where brackets can be omitted and which act on finite
lists and sets. Ser $SERIAL.
SERIAL::=http://www/dick/maths/notn_12_Expressions.html#SERIAL
. References
LAWS::=following
.Set
LAW0::=
.See [Hoareetal69]
LAW1::=
.See [Hoareetal87]
LAW2::=
.See [Hoareetal87b]
.Close.Set
Comm ACM september 87
Maddux96::=following
.Set
.See [Maddux96]
.See RELATION_ALGEBRA
.Close.Set
.Open Proofs
. Proof of c4
P<|b|>(Q<|b|>R)
=
b;P | no b;(b;Q|no b;R)
=
b;P | no b;b;Q | no b;no b;R
=
b;P | no b; R.
(P<|b|>Q)<|b|>R
=
b;b;P | b;no b;Q | no b;R
=
b;P | no b;R
=
P<|b|>(Q <|b|> R).
.Close Proofs
.Close Laws of Programming
**