equal
deleted
inserted
replaced
31 ires :: "resType" |
31 ires :: "resType" |
32 |
32 |
33 definition |
33 definition |
34 (* auxiliary predicates *) |
34 (* auxiliary predicates *) |
35 MVOKBARF :: "Vals \<Rightarrow> bool" |
35 MVOKBARF :: "Vals \<Rightarrow> bool" |
36 where "MVOKBARF v <-> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)" |
36 where "MVOKBARF v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)" |
37 |
37 |
38 definition |
38 definition |
39 MVOKBA :: "Vals \<Rightarrow> bool" |
39 MVOKBA :: "Vals \<Rightarrow> bool" |
40 where "MVOKBA v <-> (v : MemVal) | (v = OK) | (v = BadArg)" |
40 where "MVOKBA v \<longleftrightarrow> (v : MemVal) | (v = OK) | (v = BadArg)" |
41 |
41 |
42 definition |
42 definition |
43 MVNROKBA :: "Vals \<Rightarrow> bool" |
43 MVNROKBA :: "Vals \<Rightarrow> bool" |
44 where "MVNROKBA v <-> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)" |
44 where "MVNROKBA v \<longleftrightarrow> (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)" |
45 |
45 |
46 definition |
46 definition |
47 (* tuples of state functions changed by the various components *) |
47 (* tuples of state functions changed by the various components *) |
48 e :: "PrIds => (bit * memOp) stfun" |
48 e :: "PrIds => (bit * memOp) stfun" |
49 where "e p = PRED (caller memCh!p)" |
49 where "e p = PRED (caller memCh!p)" |