src/HOL/UNITY/README.html
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5461 6376d5cbb6ac
permissions -rw-r--r--
New UNITY theory
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
     3 
     4 <H2>UNITY--Chandy and Misra's UNITY formalism</H2>
     5 
     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
     8 programming language of guarded assignments and an associated calculus.
     9 Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
    10 giving more elegant foundations for a more general class of languages.
    11 
    12 <P> This directory is a preliminary formalization of New UNITY.  The Isabelle
    13 examples may not represent the most natural treatment of UNITY style.  Hand
    14 UNITY proofs tend to be written in the forwards direction, as in informal
    15 mathematics, while Isabelle works best in a backwards (goal-directed) style.
    16 
    17 <P>
    18 The syntax, also, is rather unnatural.   Programs are expressed as sets of 
    19 commands, where each command is a relation on states.  Quantification over 
    20 commands using [] is easily expressed.  At present, there are no examples of
    21 quantification using ||.
    22 
    23 <P>
    24 The directory presents a few small examples, mostly taken from Misra's 1994
    25 paper:
    26 <UL>
    27 <LI>common meeting time
    28 
    29 <LI>the token ring
    30 
    31 <LI>the communication network
    32 
    33 <LI><EM>n</EM>-process deadlock
    34 
    35 <LI>unordered channel
    36 
    37 <LI>reachability in directed graphs (section 6.4 of the book)
    38 </UL>
    39 
    40 <P> Safety proofs (invariants) are often proved automatically.  Progress
    41 proofs involving ENSURES can sometimes be proved automatically.  The
    42 level of automation appears to be about the same as in HOL-UNITY by Flemming
    43 Andersen et al.
    44 
    45 <HR>
    46 <P>Last modified on $Date$
    47 
    48 <ADDRESS>
    49 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    50 </ADDRESS>
    51 </BODY></HTML>