Algebra Unifies Calculi of Programming with Tony Hoare and Others

Algebra unifies calculi of programming Tony Hoare Feb 2012

With Ideas from Ian Wehrman John Wickerson Stephan van Staden Peter O Hearn Bernhard Moeller Georg Struth Rasmus Petersen and others

and Calculi from Robin Milner Edsger Dijkstra Ralph Back Carroll Morgan Gilles Kahn, Gordon Plotkin Cliff Jones Tony Hoare

but in this talk, only four x x Robin Milner Edsger Dijkstra Ralph Back Carroll Morgan Gilles Kahn, Gordon Plotkin Cliff Jones Tony Hoare x x

Subject matter: specs variables (p, q, r) stand for computer programs, designs, contracts, specifications, they all describe what happens inside/around a computer that executes a given program. The program itself is the most precise description giving all the excruciating detail. The user specification is the most abstract describing only interactions with environment. Designs come in between.

Example specs Postcondition: execution ends with array A sorted Conditional correctness: if execution ends, it ends with A sorted Precondition: execution starts with x even Program: x := x+1 the final value of x is one greater than the initial

More examples of specs Safety: There are no buffer overflows Termination: execution is finite (ie., always ends) Liveness: no infinite internal activity (livelock) Fairness: no infinite waiting Probability: the ration of a s to b s tends to 1 with time

Also Security low programs do not access high variables Separation threads do not assign to shared variables Communication outputs on channel c are in alphabetical order Predictability there are no race conditions timing interval between request and response is short

Advantages of unification Same laws for programs, designs, specs Same laws for many forms of correctness Tools based on the laws serve many purposes and communicate by sound interfaces Scientific controversy is resolved and engineers confidently apply the science

Operators on specs or and then while \/ /\ ; * disjunction conjunction sequential composition concurrent composition Constants terminates immediately does anything never starts skip true false I

The language model a language is a set of strings of characters /\ is set intersection \/ is set union ; is pointwise concatenation of strings * is pointwise interleaving of strings I is the language with only the empty string is set of all strings is the empty set.

Laws \/ yes yes yes T /\ yes yes yes T ; yes no no * yes yes no assoc comm unit zero

Distribution axioms ; distributes through \/ (p*q) ; (p * q ) where p => q in the language model there are less interleavings on the left of => remember the exchange law in categories? => (p;p )*(q;q ) q = p \/ q =def (refinement)

Theorems => is a partial order All the operators are monotonic (p*q);q => p*(q;q ) Proof: substitute for p in exchange (p/\q);(p /\q ) => (p;p )/\(q;q ) Proof: lhs => p;p lhs => q;q The result follows from Boolean algebra. by monotonicity of ; similarly.

Hoare triple: {p} q {r} defined as p;q => r starting in the final state of any execution of p, q ends in the final state of some execution of r (p and r may be arbitrary specs). example: {..x+1 n} x:= x + 1 {..x n} where ..b (finally b) describes all executions that end in a state satisfying a single-state predicate b .

Milner triple: r - p -> q defined as p;q => r r may be executed by first executing p and then executing q . p is usually restricted to atomic actions. example: (<a>;q) <a> -> q (same as Hoare!) where <a> is an atomic action r -> p = def. p => r an execution step may reduce non-determinism

Theorems Using these definitions, the rules of the Hoare calculus and of the Milner calculus are derivable by simple algebraic proofs from the laws of the algebra.

Rule of consequence p => p {p } q {r } {p} q {r} r => r r -> r r q-> p r q-> p p -> p Proof: ; is monotonic, => is transitive. These two rules are not only similar, they are the same!

Sequential composition {p} q {s} {s} q {r} {p} q;q {r} r q-> s s q -> p r q;q -> p Proof: associativity of ;

Small-step rule p <a>-> r (r;q ) <a>->(q;q ) {p} q {r} . {p} q;q {r;q } Proof: monotonicity of ;

Choice {p} q {r} {p} q {r} {p} (q \/ q ) {r} both choices must be correct r q-> p (r \/ r ) q-> p so the execution may make either choice

Frame Law {p} q {r} {p*f} q {r*f} adapts a rule to a wider environment f r q-> p (r*f) q-> (p*f) a step that is possible for a single thread is still possible in a wider environment f

Concurrency (and Conjunction) {p} q {r} {p } q {r } {p*p } (q * q ) {r*r } permits modular proof of concurrent programs. {p} q {r} {p } q {r } {p/\p } (q /\ q ) {r/\r } in Floyd s rule of conjunction, q = q .

Concurrency r p-> q (r*r) -(p*p )-> (q*q ) r -p -> q provided p*p = where is the unobserved transition, (which occurs (in CCS) when p and p are an input and an output on the same channel).

Dijkstra triple: p => q\r usually written: defined by: wp(q,r) = p => wlp(q,r) p;q => r (again) wlp(q, r/\ terminates) q\r specifies the weakest program which can be executed before q to achieve the overall effect of r .

Morgan triple: q => r/p defined by: p;q => r (again) r/p is the weakest program which can be executed after p to achieve r.

Theorems q\(r /\ r ) (r /\ r )/p = = (q\r) /\ (q\r ) (r/p) /\ (r /p) (q \/ q )\r r/(p \/ p ) = = (q\r) /\ (q \r) (r/p) /\ (r/p )

Theorems (q;q )\r r/(p;p ) = = q\(q \r) (r/p)/p (q\r)*(q \r ) => (q*q )\(r*r ) exchange law

Unification is the goal of every branch of pure science, because it increases conviction in theory Specialisation is needed for each application, e.g., Hoare logic: proofs of correctness, Milner: implementation, Dijkstra: program analysis, Morgan: programs from specifications

Algebra is modular, incremental, comprehensible, abstract and beautiful. An algebraic law can say as little as you like using any other concepts that you need. new properties can be added by new laws. The definition of a concept is allowed only once so it must describe all the needed properties, using only previously defined concepts. Inductive clauses restrict incrementality Algebra is good for unification

Summary: p;q => r is written p {q} r {p} q {r} r p-> q p => wlp(q,r) q => [p, r] by Hoare Wirth Milner Dijkstra Morgan (triple) (triple) (transition) (weakest precondition) (specification statement) Milner restricts p to atomic actions (small-step version). The others restrict p and r to descriptions of single states.

Conclusions All the calculi are derived from the same algebra of programming. The algebra is simpler than each of the calculi, and stronger than all of them combined.

Isaac Newton Communication with Richard Gregory (1694) Our specious algebra [of fluxions] is fit enough to find out, but entirely unfit to consign to writing and commit to posterity.