updated
authorpaulson
Tue Oct 20 11:27:06 1998 +0200 (1998-10-20)
changeset 5679916c75592bf6
parent 5678 e68c518b9140
child 5680 4f526bcd3a68
updated
src/HOL/UNITY/README.html
     1.1 --- a/src/HOL/UNITY/README.html	Tue Oct 20 11:16:23 1998 +0200
     1.2 +++ b/src/HOL/UNITY/README.html	Tue Oct 20 11:27:06 1998 +0200
     1.3 @@ -4,21 +4,24 @@
     1.4  <H2>UNITY--Chandy and Misra's UNITY formalism</H2>
     1.5  
     1.6  <P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
     1.7 -(Addison-Wesley, 1988) presents UNITY, which consists of an abstract
     1.8 -programming language of guarded assignments and an associated calculus.
     1.9 -Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
    1.10 -giving more elegant foundations for a more general class of languages.
    1.11 +(Addison-Wesley, 1988) presents the UNITY formalism.  UNITY consists of an
    1.12 +abstract programming language of guarded assignments and a calculus for
    1.13 +reasoning about such programs.  Misra's 1994 paper "A Logic for Concurrent
    1.14 +Programming" presents New UNITY, giving more elegant foundations for a more
    1.15 +general class of languages.  In recent work, Chandy and Sanders have proposed
    1.16 +new methods for reasoning about systems composed of many components.
    1.17  
    1.18 -<P> This directory is a preliminary formalization of New UNITY.  The Isabelle
    1.19 -examples may not represent the most natural treatment of UNITY style.  Hand
    1.20 -UNITY proofs tend to be written in the forwards direction, as in informal
    1.21 -mathematics, while Isabelle works best in a backwards (goal-directed) style.
    1.22 +<P>This directory formalizes these new ideas for UNITY.  The Isabelle examples
    1.23 +may seem strange to UNITY traditionalists.  Hand UNITY proofs tend to be
    1.24 +written in the forwards direction, as in informal mathematics, while Isabelle
    1.25 +works best in a backwards (goal-directed) style.  Programs are expressed as
    1.26 +sets of commands, where each command is a relation on states.  Quantification
    1.27 +over commands using [] is easily expressed.  At present, there are no examples
    1.28 +of quantification using ||.
    1.29  
    1.30 -<P>
    1.31 -The syntax, also, is rather unnatural.   Programs are expressed as sets of 
    1.32 -commands, where each command is a relation on states.  Quantification over 
    1.33 -commands using [] is easily expressed.  At present, there are no examples of
    1.34 -quantification using ||.
    1.35 +<P>A UNITY assertion denotes the set of programs satisfying it, as
    1.36 +in the propositions-as-types paradigm.  The resulting style is readable if
    1.37 +unconventional.
    1.38  
    1.39  <P>
    1.40  The directory presents a few small examples, mostly taken from Misra's 1994