| author | ballarin |
| Wed, 19 Jul 2006 19:25:58 +0200 | |
| changeset 20168 | ed7bced29e1b |
| parent 15582 | 7219facb3fd0 |
| child 51404 | 90a598019aeb |
| permissions | -rw-r--r-- |
| 15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
| 4776 | 3 |
<!-- $Id$ --> |
| 15582 | 4 |
|
5 |
<HTML> |
|
6 |
||
7 |
<HEAD> |
|
8 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
9 |
<TITLE>HOL/UNITY/README</TITLE> |
|
10 |
</HEAD> |
|
11 |
||
12 |
<BODY> |
|
| 4776 | 13 |
|
14 |
<H2>UNITY--Chandy and Misra's UNITY formalism</H2> |
|
15 |
||
16 |
<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra |
|
| 5679 | 17 |
(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an |
18 |
abstract programming language of guarded assignments and a calculus for |
|
19 |
reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent |
|
20 |
Programming" presents New UNITY, giving more elegant foundations for a more |
|
21 |
general class of languages. In recent work, Chandy and Sanders have proposed |
|
22 |
new methods for reasoning about systems composed of many components. |
|
| 4776 | 23 |
|
| 5679 | 24 |
<P>This directory formalizes these new ideas for UNITY. The Isabelle examples |
25 |
may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be |
|
26 |
written in the forwards direction, as in informal mathematics, while Isabelle |
|
27 |
works best in a backwards (goal-directed) style. Programs are expressed as |
|
28 |
sets of commands, where each command is a relation on states. Quantification |
|
29 |
over commands using [] is easily expressed. At present, there are no examples |
|
30 |
of quantification using ||. |
|
| 4776 | 31 |
|
| 5679 | 32 |
<P>A UNITY assertion denotes the set of programs satisfying it, as |
33 |
in the propositions-as-types paradigm. The resulting style is readable if |
|
34 |
unconventional. |
|
| 4776 | 35 |
|
36 |
<P> Safety proofs (invariants) are often proved automatically. Progress |
|
37 |
proofs involving ENSURES can sometimes be proved automatically. The |
|
38 |
level of automation appears to be about the same as in HOL-UNITY by Flemming |
|
39 |
Andersen et al. |
|
40 |
||
|
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
41 |
<P> |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
paper, involving single programs. |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
45 |
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
|
46 |
presents examples of proofs involving program composition. |
|
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
5679
diff
changeset
|
47 |
|
| 4776 | 48 |
<HR> |
49 |
<P>Last modified on $Date$ |
|
50 |
||
51 |
<ADDRESS> |
|
52 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
53 |
</ADDRESS> |
|
54 |
</BODY></HTML> |