src/HOL/UNITY/README.html
author paulson
Thu Sep 10 17:30:50 1998 +0200 (1998-09-10)
changeset 5461 6376d5cbb6ac
parent 4776 1f9362e769c1
child 5679 916c75592bf6
permissions -rw-r--r--
new entries
     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>the lift controller (a standard benchmark)
    34 
    35 <LI>a mutual exclusion algorithm
    36 
    37 <LI><EM>n</EM>-process deadlock
    38 
    39 <LI>unordered channel
    40 
    41 <LI>reachability in directed graphs (section 6.4 of the book)
    42 </UL>
    43 
    44 <P> Safety proofs (invariants) are often proved automatically.  Progress
    45 proofs involving ENSURES can sometimes be proved automatically.  The
    46 level of automation appears to be about the same as in HOL-UNITY by Flemming
    47 Andersen et al.
    48 
    49 <HR>
    50 <P>Last modified on $Date$
    51 
    52 <ADDRESS>
    53 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    54 </ADDRESS>
    55 </BODY></HTML>