11479
|
1 |
(* Title: ZF/UNITY/Guar.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
|
|
6 |
Guarantees, etc.
|
|
7 |
|
|
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 |
|
|
19 |
Theory ported from HOL.
|
|
20 |
*)
|
|
21 |
Guar = Comp +
|
|
22 |
constdefs
|
|
23 |
|
|
24 |
(*Existential and Universal properties. I formalize the two-program
|
|
25 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*)
|
|
26 |
|
|
27 |
ex_prop :: i =>o
|
12195
|
28 |
"ex_prop(X) == X<=program &
|
|
29 |
(ALL F:program. ALL G:program. F ok G --> F:X | G:X --> (F Join G):X)"
|
11479
|
30 |
|
|
31 |
strict_ex_prop :: i => o
|
12195
|
32 |
"strict_ex_prop(X) == X<=program &
|
|
33 |
(ALL F:program. ALL G:program. F ok G --> (F:X | G: X) <-> (F Join G : X))"
|
11479
|
34 |
|
|
35 |
uv_prop :: i => o
|
12195
|
36 |
"uv_prop(X) == X<=program &
|
|
37 |
(SKIP:X & (ALL F:program. ALL G:program. F ok G --> F:X & G:X --> (F Join G):X))"
|
11479
|
38 |
|
|
39 |
strict_uv_prop :: i => o
|
12195
|
40 |
"strict_uv_prop(X) == X<=program &
|
|
41 |
(SKIP:X & (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X)))"
|
11479
|
42 |
|
|
43 |
guar :: [i, i] => i (infixl "guarantees" 55)
|
|
44 |
(*higher than membership, lower than Co*)
|
|
45 |
"X guarantees Y == {F:program. ALL G:program. F ok G --> F Join G : X --> F Join G:Y}"
|
|
46 |
|
|
47 |
(* Weakest guarantees *)
|
|
48 |
wg :: [i,i] => i
|
|
49 |
"wg(F,Y) == Union({X:Pow(program). F:(X guarantees Y)})"
|
|
50 |
|
|
51 |
(* Weakest existential property stronger than X *)
|
|
52 |
wx :: "i =>i"
|
|
53 |
"wx(X) == Union({Y:Pow(program). Y<=X & ex_prop(Y)})"
|
|
54 |
|
|
55 |
(*Ill-defined programs can arise through "Join"*)
|
|
56 |
welldef :: i
|
|
57 |
"welldef == {F:program. Init(F) ~= 0}"
|
|
58 |
|
|
59 |
refines :: [i, i, i] => o ("(3_ refines _ wrt _)" [10,10,10] 10)
|
|
60 |
"G refines F wrt X ==
|
|
61 |
ALL H:program. (F ok H & G ok H & F Join H:welldef Int X)
|
|
62 |
--> (G Join H:welldef Int X)"
|
|
63 |
|
|
64 |
iso_refines :: [i,i, i] => o ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
|
|
65 |
"G iso_refines F wrt X == F:welldef Int X --> G:welldef Int X"
|
|
66 |
|
|
67 |
end
|