fixed the merge spec (NbT -> Nclients) and added the distributor spec
authorpaulson
Thu Jun 22 11:35:28 2000 +0200 (2000-06-22)
changeset 9105d9257992b845
parent 9104 89ca2a172f84
child 9106 0fe9200f64bd
fixed the merge spec (NbT -> Nclients) and added the distributor spec
src/HOL/UNITY/AllocImpl.thy
     1.1 --- a/src/HOL/UNITY/AllocImpl.thy	Thu Jun 22 11:34:48 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocImpl.thy	Thu Jun 22 11:35:28 2000 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -(** Merge specification (NbT is the number of inputs) ***)
     1.8 +(** Merge specification (the number of inputs is Nclients) ***)
     1.9  
    1.10    (*spec (10)*)
    1.11    merge_increasing :: ('a,'b) merge_u program set
    1.12 @@ -74,7 +74,7 @@
    1.13    merge_bounded :: ('a,'b) merge_u program set
    1.14      "merge_bounded ==
    1.15           UNIV guarantees[merge.iOut]
    1.16 -         Always {s. ALL elt : set (merge.iOut s). elt <= NbT}"
    1.17 +         Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
    1.18  
    1.19    (*spec (13)*)
    1.20    merge_follows :: ('a,'b) merge_u program set
    1.21 @@ -83,15 +83,9 @@
    1.22  	 guarantees[funPair merge.Out merge.iOut]
    1.23  	 (INT i : lessThan Nclients. 
    1.24  	  (%s. sublist (merge.Out s) 
    1.25 -                       {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
    1.26 +                       {k. k < size(merge.iOut s) & merge.iOut s! k = i})
    1.27  	  Fols (sub i o merge.In))"
    1.28  
    1.29 -(*
    1.30 -	  (%s. map fst (filter (%p. snd p = i)
    1.31 -			(zip (merge.Out s) (merge.iOut s))))
    1.32 -	  Fols (sub i o merge.In)
    1.33 -*)
    1.34 -
    1.35    (*spec: preserves part*)
    1.36      merge_preserves :: ('a,'b) merge_u program set
    1.37      "merge_preserves == preserves (funPair merge.In merge_u.extra)"
    1.38 @@ -100,6 +94,20 @@
    1.39      "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
    1.40                     merge_follows Int merge_preserves"
    1.41  
    1.42 +(** Distributor specification (the number of outputs is Nclients) ***)
    1.43 +
    1.44 +  (*spec (14)*)
    1.45 +  distr_follows :: ('a,'b) distr_u program set
    1.46 +    "distr_follows ==
    1.47 +	 Increasing distr.In Int Increasing distr.iIn Int
    1.48 +	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
    1.49 +	 guarantees[distr.Out]
    1.50 +	 (INT i : lessThan Nclients. 
    1.51 +	  (sub i o distr.Out) Fols
    1.52 +	  (%s. sublist (distr.In s) 
    1.53 +                       {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
    1.54 +
    1.55 +
    1.56  (** Single-client allocator specification (required) ***)
    1.57  
    1.58    (*spec (18)*)