author | haftmann |
Mon, 05 Jul 2010 15:12:20 +0200 | |
changeset 37714 | 2eb2b048057b |
parent 32624 | 3dec57ec3473 |
permissions | -rw-r--r-- |
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
1 |
(* Author: Lawrence C Paulson Cambridge University Computer Laboratory |
4776 | 2 |
Copyright 1998 University of Cambridge |
3 |
*) |
|
4 |
||
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
5 |
header {* Various examples for UNITY *} |
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
6 |
|
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
7 |
theory UNITY_Examples |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
8 |
imports |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
9 |
UNITY_Main |
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
10 |
|
24147 | 11 |
(*Simple examples: no composition*) |
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
12 |
"Simple/Deadlock" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
13 |
"Simple/Common" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
14 |
"Simple/Network" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
15 |
"Simple/Token" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
16 |
"Simple/Channel" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
17 |
"Simple/Lift" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
18 |
"Simple/Mutex" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
19 |
"Simple/Reach" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
20 |
"Simple/Reachability" |
11193
851c90b23a9e
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
10782
diff
changeset
|
21 |
|
24147 | 22 |
(*Verifying security protocols using UNITY*) |
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
23 |
"Simple/NSP_Bad" |
9112 | 24 |
|
24147 | 25 |
(*Example of composition*) |
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
26 |
"Comp/Handshake" |
10782 | 27 |
|
24147 | 28 |
(*Universal properties examples*) |
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
29 |
"Comp/Counter" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
30 |
"Comp/Counterc" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
31 |
"Comp/Priority" |
24147 | 32 |
|
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
33 |
"Comp/TimerArray" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
34 |
"Comp/Progress" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
35 |
|
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
36 |
"Comp/Alloc" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
37 |
"Comp/AllocImpl" |
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
38 |
"Comp/Client" |
24147 | 39 |
|
40 |
(*obsolete*) |
|
41 |
"ELT" |
|
9112 | 42 |
|
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
43 |
begin |
8987 | 44 |
|
32624
3dec57ec3473
entry point theory for examples; reactivated half-dead example
haftmann
parents:
28866
diff
changeset
|
45 |
end |