src/HOL/UNITY/README.html
author paulson
Tue Feb 01 18:01:57 2005 +0100 (2005-02-01)
changeset 15481 fc075ae929e4
parent 15283 f21466450330
child 15582 7219facb3fd0
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
     5 
     6 <H2>UNITY--Chandy and Misra's UNITY formalism</H2>
     7 
     8 <P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
     9 (Addison-Wesley, 1988) presents the UNITY formalism.  UNITY consists of an
    10 abstract programming language of guarded assignments and a calculus for
    11 reasoning about such programs.  Misra's 1994 paper "A Logic for Concurrent
    12 Programming" presents New UNITY, giving more elegant foundations for a more
    13 general class of languages.  In recent work, Chandy and Sanders have proposed
    14 new methods for reasoning about systems composed of many components.
    15 
    16 <P>This directory formalizes these new ideas for UNITY.  The Isabelle examples
    17 may seem strange to UNITY traditionalists.  Hand UNITY proofs tend to be
    18 written in the forwards direction, as in informal mathematics, while Isabelle
    19 works best in a backwards (goal-directed) style.  Programs are expressed as
    20 sets of commands, where each command is a relation on states.  Quantification
    21 over commands using [] is easily expressed.  At present, there are no examples
    22 of quantification using ||.
    23 
    24 <P>A UNITY assertion denotes the set of programs satisfying it, as
    25 in the propositions-as-types paradigm.  The resulting style is readable if
    26 unconventional.
    27 
    28 <P> Safety proofs (invariants) are often proved automatically.  Progress
    29 proofs involving ENSURES can sometimes be proved automatically.  The
    30 level of automation appears to be about the same as in HOL-UNITY by Flemming
    31 Andersen et al.
    32 
    33 <P>
    34 The directory <A HREF="Simple/"><CODE>Simple</CODE></A>
    35 presents a few examples, mostly taken from Misra's 1994
    36 paper, involving single programs.
    37 The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
    38 presents examples of proofs involving program composition.
    39 
    40 <HR>
    41 <P>Last modified on $Date$
    42 
    43 <ADDRESS>
    44 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    45 </ADDRESS>
    46 </BODY></HTML>