<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
(Addison-Wesley, 1988) presents UNITY, which consists of an abstract
programming language of guarded assignments and an associated calculus.
Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
giving more elegant foundations for a more general class of languages.
<P> This directory is a preliminary formalization of New UNITY. The Isabelle
examples may not represent the most natural treatment of UNITY style. Hand
UNITY proofs tend to be written in the forwards direction, as in informal
mathematics, while Isabelle works best in a backwards (goal-directed) style.
<P>
The syntax, also, is rather unnatural. Programs are expressed as sets of
commands, where each command is a relation on states. Quantification over
commands using [] is easily expressed. At present, there are no examples of
quantification using ||.
<P>
The directory presents a few small examples, mostly taken from Misra's 1994
paper:
<UL>
<LI>common meeting time
<LI>the token ring
<LI>the communication network
<LI><EM>n</EM>-process deadlock
<LI>unordered channel
<LI>reachability in directed graphs (section 6.4 of the book)
</UL>
<P> Safety proofs (invariants) are often proved automatically. Progress
proofs involving ENSURES can sometimes be proved automatically. The
level of automation appears to be about the same as in HOL-UNITY by Flemming
Andersen et al.
<HR>
<P>Last modified on $Date$
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>