6 The basic UNITY theory (revised version, based upon the "co" operator) |
6 The basic UNITY theory (revised version, based upon the "co" operator) |
7 |
7 |
8 From Misra, "A Logic for Concurrent Programming", 1994 |
8 From Misra, "A Logic for Concurrent Programming", 1994 |
9 *) |
9 *) |
10 |
10 |
11 UNITY = LessThan + |
11 UNITY = Traces + Prefix + |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
15 constrains :: "['a set, 'a set] => 'a program set" |
16 "constrains acts A B == ALL act:acts. act^^A <= B" |
16 "constrains A B == {F. ALL act: Acts F. act^^A <= B}" |
17 |
17 |
18 stable :: "('a * 'a)set set => 'a set => bool" |
18 stable :: "'a set => 'a program set" |
19 "stable acts A == constrains acts A A" |
19 "stable A == constrains A A" |
20 |
20 |
21 strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" |
21 strongest_rhs :: "['a program, 'a set] => 'a set" |
22 "strongest_rhs acts A == Inter {B. constrains acts A B}" |
22 "strongest_rhs F A == Inter {B. F : constrains A B}" |
23 |
23 |
24 unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 unless :: "['a set, 'a set] => 'a program set" |
25 "unless acts A B == constrains acts (A-B) (A Un B)" |
25 "unless A B == constrains (A-B) (A Un B)" |
|
26 |
|
27 (*The traditional word for inductive properties. Anyway, INDUCTIVE is |
|
28 reserved!*) |
|
29 invariant :: "'a set => 'a program set" |
|
30 "invariant A == {F. Init F <= A} Int stable A" |
|
31 |
|
32 (*Safety properties*) |
|
33 always :: "'a set => 'a program set" |
|
34 "always A == {F. reachable F <= A}" |
|
35 |
|
36 (*Polymorphic in both states and the meaning of <= *) |
|
37 increasing :: "['a => 'b::{ord}] => 'a program set" |
|
38 "increasing f == INT z. stable {s. z <= f s}" |
26 |
39 |
27 end |
40 end |