NameDateSize

..25-Jul-2019169

Comp/H25-Jul-201914

Comp.thyH A D25-Jul-20198 KiB

Constrains.thyH A D25-Jul-201914.2 KiB

Detects.thyH A D25-Jul-20192.7 KiB

document/H25-Jul-20193

ELT.thyH A D25-Jul-201922.1 KiB

Extend.thyH A D25-Jul-201923.3 KiB

Follows.thyH A D25-Jul-20199.3 KiB

FP.thyH A D25-Jul-20191.7 KiB

Guar.thyH A D25-Jul-201916.8 KiB

Lift_prog.thyH A D25-Jul-201914 KiB

ListOrder.thyH A D25-Jul-201912.3 KiB

PPROD.thyH A D25-Jul-20199.8 KiB

ProgressSets.thyH A D25-Jul-201922.5 KiB

Project.thyH A D25-Jul-201924.8 KiB

README.htmlH A D25-Jul-20192 KiB

Rename.thyH A D25-Jul-201913 KiB

Simple/H25-Jul-201913

SubstAx.thyH A D25-Jul-201914.3 KiB

Transformers.thyH A D25-Jul-201919 KiB

Union.thyH A D25-Jul-201916.3 KiB

UNITY.thyH A D25-Jul-201915.5 KiB

UNITY_Main.thyH A D25-Jul-2019917

UNITY_tactics.MLH A D25-Jul-20192.6 KiB

WFair.thyH A D25-Jul-201922.7 KiB

README.html

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