summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/UNITY/README.html

changeset 5679 | 916c75592bf6 |

parent 5461 | 6376d5cbb6ac |

child 11193 | 851c90b23a9e |

1.1 --- a/src/HOL/UNITY/README.html Tue Oct 20 11:16:23 1998 +0200 1.2 +++ b/src/HOL/UNITY/README.html Tue Oct 20 11:27:06 1998 +0200 1.3 @@ -4,21 +4,24 @@ 1.4 <H2>UNITY--Chandy and Misra's UNITY formalism</H2> 1.5 1.6 <P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra 1.7 -(Addison-Wesley, 1988) presents UNITY, which consists of an abstract 1.8 -programming language of guarded assignments and an associated calculus. 1.9 -Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY", 1.10 -giving more elegant foundations for a more general class of languages. 1.11 +(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an 1.12 +abstract programming language of guarded assignments and a calculus for 1.13 +reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent 1.14 +Programming" presents New UNITY, giving more elegant foundations for a more 1.15 +general class of languages. In recent work, Chandy and Sanders have proposed 1.16 +new methods for reasoning about systems composed of many components. 1.17 1.18 -<P> This directory is a preliminary formalization of New UNITY. The Isabelle 1.19 -examples may not represent the most natural treatment of UNITY style. Hand 1.20 -UNITY proofs tend to be written in the forwards direction, as in informal 1.21 -mathematics, while Isabelle works best in a backwards (goal-directed) style. 1.22 +<P>This directory formalizes these new ideas for UNITY. The Isabelle examples 1.23 +may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be 1.24 +written in the forwards direction, as in informal mathematics, while Isabelle 1.25 +works best in a backwards (goal-directed) style. Programs are expressed as 1.26 +sets of commands, where each command is a relation on states. Quantification 1.27 +over commands using [] is easily expressed. At present, there are no examples 1.28 +of quantification using ||. 1.29 1.30 -<P> 1.31 -The syntax, also, is rather unnatural. Programs are expressed as sets of 1.32 -commands, where each command is a relation on states. Quantification over 1.33 -commands using [] is easily expressed. At present, there are no examples of 1.34 -quantification using ||. 1.35 +<P>A UNITY assertion denotes the set of programs satisfying it, as 1.36 +in the propositions-as-types paradigm. The resulting style is readable if 1.37 +unconventional. 1.38 1.39 <P> 1.40 The directory presents a few small examples, mostly taken from Misra's 1994