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