author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11190 | 44e157622cb2 |
child 13792 | d1811693899c |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.thy |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
5 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
6 |
Guarantees, etc. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
7 |
|
11190 | 8 |
From Chandy and Sanders, "Reasoning About Program Composition", |
9 |
Technical Report 2000-003, University of Florida, 2000. |
|
10 |
||
11 |
Revised by Sidi Ehmety on January 2001 |
|
12 |
||
13 |
Added: Compatibility, weakest guarantees, etc. |
|
14 |
||
15 |
and Weakest existential property, |
|
16 |
from Charpentier and Chandy "Theorems about Composition", |
|
17 |
Fifth International Conference on Mathematics of Program, 2000. |
|
18 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
19 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
20 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
21 |
Guar = Comp + |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
22 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11190
diff
changeset
|
23 |
instance program :: (type) order |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
24 |
(component_refl, component_trans, component_antisym, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
25 |
program_less_le) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
26 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
27 |
constdefs |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
28 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
29 |
(*Existential and Universal properties. I formalize the two-program |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
30 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
31 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
32 |
ex_prop :: 'a program set => bool |
11190 | 33 |
"ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
34 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
35 |
strict_ex_prop :: 'a program set => bool |
11190 | 36 |
"strict_ex_prop X == ALL F G. F ok G --> (F:X | G: X) = (F Join G : X)" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
37 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
38 |
uv_prop :: 'a program set => bool |
11190 | 39 |
"uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
40 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
41 |
strict_uv_prop :: 'a program set => bool |
11190 | 42 |
"strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))" |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
43 |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
44 |
guar :: ['a program set, 'a program set] => 'a program set |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
45 |
(infixl "guarantees" 55) (*higher than membership, lower than Co*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9337
diff
changeset
|
46 |
"X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}" |
11190 | 47 |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
48 |
|
11190 | 49 |
(* Weakest guarantees *) |
50 |
wg :: ['a program, 'a program set] => 'a program set |
|
51 |
"wg F Y == Union({X. F:X guarantees Y})" |
|
52 |
||
53 |
(* Weakest existential property stronger than X *) |
|
54 |
wx :: "('a program) set => ('a program)set" |
|
55 |
"wx X == Union({Y. Y<=X & ex_prop Y})" |
|
56 |
||
57 |
(*Ill-defined programs can arise through "Join"*) |
|
58 |
welldef :: 'a program set |
|
59 |
"welldef == {F. Init F ~= {}}" |
|
60 |
||
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
61 |
refines :: ['a program, 'a program, 'a program set] => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
62 |
("(3_ refines _ wrt _)" [10,10,10] 10) |
11190 | 63 |
"G refines F wrt X == |
64 |
ALL H. (F ok H & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
65 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
66 |
iso_refines :: ['a program, 'a program, 'a program set] => bool |
11190 | 67 |
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) |
68 |
"G iso_refines F wrt X == |
|
69 |
F : welldef Int X --> G : welldef Int X" |
|
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
70 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
71 |
end |