src/HOL/UNITY/README.html
author paulson
Tue Oct 20 11:27:06 1998 +0200 (1998-10-20)
changeset 5679 916c75592bf6
parent 5461 6376d5cbb6ac
child 11193 851c90b23a9e
permissions -rw-r--r--
updated
     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 the UNITY formalism.  UNITY consists of an
     8 abstract programming language of guarded assignments and a calculus for
     9 reasoning about such programs.  Misra's 1994 paper "A Logic for Concurrent
    10 Programming" presents New UNITY, giving more elegant foundations for a more
    11 general class of languages.  In recent work, Chandy and Sanders have proposed
    12 new methods for reasoning about systems composed of many components.
    13 
    14 <P>This directory formalizes these new ideas for UNITY.  The Isabelle examples
    15 may seem strange to UNITY traditionalists.  Hand UNITY proofs tend to be
    16 written in the forwards direction, as in informal mathematics, while Isabelle
    17 works best in a backwards (goal-directed) style.  Programs are expressed as
    18 sets of commands, where each command is a relation on states.  Quantification
    19 over commands using [] is easily expressed.  At present, there are no examples
    20 of quantification using ||.
    21 
    22 <P>A UNITY assertion denotes the set of programs satisfying it, as
    23 in the propositions-as-types paradigm.  The resulting style is readable if
    24 unconventional.
    25 
    26 <P>
    27 The directory presents a few small examples, mostly taken from Misra's 1994
    28 paper:
    29 <UL>
    30 <LI>common meeting time
    31 
    32 <LI>the token ring
    33 
    34 <LI>the communication network
    35 
    36 <LI>the lift controller (a standard benchmark)
    37 
    38 <LI>a mutual exclusion algorithm
    39 
    40 <LI><EM>n</EM>-process deadlock
    41 
    42 <LI>unordered channel
    43 
    44 <LI>reachability in directed graphs (section 6.4 of the book)
    45 </UL>
    46 
    47 <P> Safety proofs (invariants) are often proved automatically.  Progress
    48 proofs involving ENSURES can sometimes be proved automatically.  The
    49 level of automation appears to be about the same as in HOL-UNITY by Flemming
    50 Andersen et al.
    51 
    52 <HR>
    53 <P>Last modified on $Date$
    54 
    55 <ADDRESS>
    56 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    57 </ADDRESS>
    58 </BODY></HTML>