| author | paulson |
| Sun, 15 Feb 2004 10:46:37 +0100 | |
| changeset 14387 | e96d5c42c4b0 |
| parent 11195 | 65ede8dfe304 |
| child 15283 | f21466450330 |
| permissions | -rw-r--r-- |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
1 |
<!-- $Id$ --> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
<H2>UNITY: Examples Involving Single Programs</H2> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
<P> The directory presents verification examples that do not involve program |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
<UL> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
10 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
12 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
<LI>the communication network |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
15 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
17 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
18 |
<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
<LI><EM>n</EM>-process deadlock |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
<LI>reachability in directed graphs (section 6.4 of the book) (<A |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
26 |
HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
27 |
<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>) |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
28 |
</UL> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
<HR> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
<P>Last modified on $Date$ |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
32 |
|
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
<ADDRESS> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
34 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
35 |
</ADDRESS> |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
36 |
</BODY></HTML> |