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