--- a/src/HOL/UNITY/AllocImpl.thy Thu Jun 22 11:34:48 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy Thu Jun 22 11:35:28 2000 +0200
@@ -56,7 +56,7 @@
constdefs
-(** Merge specification (NbT is the number of inputs) ***)
+(** Merge specification (the number of inputs is Nclients) ***)
(*spec (10)*)
merge_increasing :: ('a,'b) merge_u program set
@@ -74,7 +74,7 @@
merge_bounded :: ('a,'b) merge_u program set
"merge_bounded ==
UNIV guarantees[merge.iOut]
- Always {s. ALL elt : set (merge.iOut s). elt <= NbT}"
+ Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
(*spec (13)*)
merge_follows :: ('a,'b) merge_u program set
@@ -83,15 +83,9 @@
guarantees[funPair merge.Out merge.iOut]
(INT i : lessThan Nclients.
(%s. sublist (merge.Out s)
- {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
+ {k. k < size(merge.iOut s) & merge.iOut s! k = i})
Fols (sub i o merge.In))"
-(*
- (%s. map fst (filter (%p. snd p = i)
- (zip (merge.Out s) (merge.iOut s))))
- Fols (sub i o merge.In)
-*)
-
(*spec: preserves part*)
merge_preserves :: ('a,'b) merge_u program set
"merge_preserves == preserves (funPair merge.In merge_u.extra)"
@@ -100,6 +94,20 @@
"merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
merge_follows Int merge_preserves"
+(** Distributor specification (the number of outputs is Nclients) ***)
+
+ (*spec (14)*)
+ distr_follows :: ('a,'b) distr_u program set
+ "distr_follows ==
+ Increasing distr.In Int Increasing distr.iIn Int
+ Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
+ guarantees[distr.Out]
+ (INT i : lessThan Nclients.
+ (sub i o distr.Out) Fols
+ (%s. sublist (distr.In s)
+ {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
+
+
(** Single-client allocator specification (required) ***)
(*spec (18)*)