equal
deleted
inserted
replaced
32 "welldef == {F. Init F ~= {}}" |
32 "welldef == {F. Init F ~= {}}" |
33 |
33 |
34 component :: ['a program, 'a program] => bool (infixl 50) |
34 component :: ['a program, 'a program] => bool (infixl 50) |
35 "F component H == EX G. F Join G = H" |
35 "F component H == EX G. F Join G = H" |
36 |
36 |
37 guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65) |
37 guarantees :: ['a program set, 'a program set] => 'a program set |
38 "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}" |
38 (infixl "guar" 65) |
|
39 "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}" |
39 |
40 |
40 refines :: ['a program, 'a program, 'a program set] => bool |
41 refines :: ['a program, 'a program, 'a program set] => bool |
41 ("(3_ refines _ wrt _)" [10,10,10] 10) |
42 ("(3_ refines _ wrt _)" [10,10,10] 10) |
42 "G refines F wrt X == |
43 "G refines F wrt X == |
43 ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X" |
44 ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X" |