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