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