1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 2 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> 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 15(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an 16abstract programming language of guarded assignments and a calculus for 17reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent 18Programming" presents New UNITY, giving more elegant foundations for a more 19general class of languages. In recent work, Chandy and Sanders have proposed 20new methods for reasoning about systems composed of many components. 21 22<P>This directory formalizes these new ideas for UNITY. The Isabelle examples 23may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be 24written in the forwards direction, as in informal mathematics, while Isabelle 25works best in a backwards (goal-directed) style. Programs are expressed as 26sets of commands, where each command is a relation on states. Quantification 27over commands using [] is easily expressed. At present, there are no examples 28of quantification using ||. 29 30<P>A UNITY assertion denotes the set of programs satisfying it, as 31in the propositions-as-types paradigm. The resulting style is readable if 32unconventional. 33 34<P> Safety proofs (invariants) are often proved automatically. Progress 35proofs involving ENSURES can sometimes be proved automatically. The 36level of automation appears to be about the same as in HOL-UNITY by Flemming 37Andersen et al. 38 39<P> 40The directory <A HREF="Simple/"><CODE>Simple</CODE></A> 41presents a few examples, mostly taken from Misra's 1994 42paper, involving single programs. 43The directory <A HREF="Comp/"><CODE>Comp</CODE></A> 44presents examples of proofs involving program composition. 45 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> 50