2 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
2 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
3 |
3 |
4 <H2>UNITY--Chandy and Misra's UNITY formalism</H2> |
4 <H2>UNITY--Chandy and Misra's UNITY formalism</H2> |
5 |
5 |
6 <P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra |
6 <P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra |
7 (Addison-Wesley, 1988) presents UNITY, which consists of an abstract |
7 (Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an |
8 programming language of guarded assignments and an associated calculus. |
8 abstract programming language of guarded assignments and a calculus for |
9 Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY", |
9 reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent |
10 giving more elegant foundations for a more general class of languages. |
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. |
11 |
13 |
12 <P> This directory is a preliminary formalization of New UNITY. The Isabelle |
14 <P>This directory formalizes these new ideas for UNITY. The Isabelle examples |
13 examples may not represent the most natural treatment of UNITY style. Hand |
15 may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be |
14 UNITY proofs tend to be written in the forwards direction, as in informal |
16 written in the forwards direction, as in informal mathematics, while Isabelle |
15 mathematics, while Isabelle works best in a backwards (goal-directed) style. |
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 ||. |
16 |
21 |
17 <P> |
22 <P>A UNITY assertion denotes the set of programs satisfying it, as |
18 The syntax, also, is rather unnatural. Programs are expressed as sets of |
23 in the propositions-as-types paradigm. The resulting style is readable if |
19 commands, where each command is a relation on states. Quantification over |
24 unconventional. |
20 commands using [] is easily expressed. At present, there are no examples of |
|
21 quantification using ||. |
|
22 |
25 |
23 <P> |
26 <P> |
24 The directory presents a few small examples, mostly taken from Misra's 1994 |
27 The directory presents a few small examples, mostly taken from Misra's 1994 |
25 paper: |
28 paper: |
26 <UL> |
29 <UL> |