| author | paulson |
| Mon, 05 Mar 2001 15:25:11 +0100 | |
| changeset 11193 | 851c90b23a9e |
| parent 5679 | 916c75592bf6 |
| child 15283 | f21466450330 |
| permissions | -rw-r--r-- |
| 4776 | 1 |
<!-- $Id$ --> |
2 |
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
|
3 |
||
4 |
<H2>UNITY--Chandy and Misra's UNITY formalism</H2> |
|
5 |
||
6 |
<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra |
|
| 5679 | 7 |
(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an |
8 |
abstract programming language of guarded assignments and a calculus for |
|
9 |
reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent |
|
10 |
Programming" presents New UNITY, giving more elegant foundations for a more |
|
11 |
general class of languages. In recent work, Chandy and Sanders have proposed |
|
12 |
new methods for reasoning about systems composed of many components. |
|
| 4776 | 13 |
|
| 5679 | 14 |
<P>This directory formalizes these new ideas for UNITY. The Isabelle examples |
15 |
may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be |
|
16 |
written in the forwards direction, as in informal mathematics, while Isabelle |
|
17 |
works best in a backwards (goal-directed) style. Programs are expressed as |
|
18 |
sets of commands, where each command is a relation on states. Quantification |
|
19 |
over commands using [] is easily expressed. At present, there are no examples |
|
20 |
of quantification using ||. |
|
| 4776 | 21 |
|
| 5679 | 22 |
<P>A UNITY assertion denotes the set of programs satisfying it, as |
23 |
in the propositions-as-types paradigm. The resulting style is readable if |
|
24 |
unconventional. |
|
| 4776 | 25 |
|
26 |
<P> Safety proofs (invariants) are often proved automatically. Progress |
|
27 |
proofs involving ENSURES can sometimes be proved automatically. The |
|
28 |
level of automation appears to be about the same as in HOL-UNITY by Flemming |
|
29 |
Andersen et al. |
|
30 |
||
|
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
31 |
<P> |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
32 |
The directory <A HREF="Simple/"><CODE>Simple</CODE></A> |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
33 |
presents a few examples, mostly taken from Misra's 1994 |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
34 |
paper, involving single programs. |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
35 |
The directory <A HREF="Comp/"><CODE>Comp</CODE></A> |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
36 |
presents examples of proofs involving program composition. |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
37 |
|
| 4776 | 38 |
<HR> |
39 |
<P>Last modified on $Date$ |
|
40 |
||
41 |
<ADDRESS> |
|
42 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
43 |
</ADDRESS> |
|
44 |
</BODY></HTML> |