Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/UNITY/Comp/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 14 kB

Quelle AllocImpl.thy Sprache: Isabelle

(*  Title:      HOL/UNITY/Comp/AllocImpl.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>

theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin

(** State definitions.  OUTPUT variables are locals **)

(*Type variable 'b is the type of items being merged*)
record 'b merge =
  In   :: "nat => 'b list"  (*merge's INPUT histories: streams to merge*)
  Out  :: "'b list"         (*merge's OUTPUT history: merged items*)
  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)

record ('a,'b) merge_d =
  "'b merge" +
  dummy :: 'a (*dummy field for new variables*)

definition non_dummy :: "('a,'b) merge_d => 'b merge" where
    "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)"

record 'b distr =
  In  :: "'b list"          (*items to distribute*)
  iIn :: "nat list"         (*destinations of items to distribute*)
  Out :: "nat => 'b list"   (*distributed items*)

record ('a,'b) distr_d =
  "'b distr" +
  dummy :: 'a (*dummy field for new variables*)

record allocState =
  giv :: "nat list"   (*OUTPUT history: source of tokens*)
  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
  rel :: "nat list"   (*INPUT: tokens released to allocator*)

record 'a allocState_d =
  allocState +
  dummy    :: 'a (*dummy field for new variables*)

record 'a systemState =
  allocState +
  mergeRel :: "nat merge"
  mergeAsk :: "nat merge"
  distr    :: "nat distr"
  dummy    :: 'a (*dummy field for new variables*)

(** Merge specification (the number of inputs is Nclients) ***)

definition
  (*spec (10)*)
  merge_increasing :: "('a,'b) merge_d program set"
  where "merge_increasing =
         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"

definition
  (*spec (11)*)
  merge_eqOut :: "('a,'b) merge_d program set"
  where "merge_eqOut =
         UNIV guarantees
         Always {s. length (merge.Out s) = length (merge.iOut s)}"

definition
  (*spec (12)*)
  merge_bounded :: "('a,'b) merge_d program set"
  where "merge_bounded =
         UNIV guarantees
         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"

definition
  (*spec (13)*)
  merge_follows :: "('a,'b) merge_d program set"
  where "merge_follows =
         (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
         guarantees
         (\<Inter>i \<in> lessThan Nclients.
          (%s. nths (merge.Out s)
                       {k. k < size(merge.iOut s) & merge.iOut s! k = i})
          Fols (sub i o merge.In))"

definition
  (*spec: preserves part*)
  merge_preserves :: "('a,'b) merge_d program set"
  where "merge_preserves = preserves merge.In Int preserves merge_d.dummy"

definition
  (*environmental constraints*)
  merge_allowed_acts :: "('a,'b) merge_d program set"
  where "merge_allowed_acts =
       {F. AllowedActs F =
            insert Id (\<Union> (Acts ` preserves (funPair merge.Out iOut)))}"

definition
  merge_spec :: "('a,'b) merge_d program set"
  where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int
                   merge_follows Int merge_allowed_acts Int merge_preserves"

(** Distributor specification (the number of outputs is Nclients) ***)

definition
  (*spec (14)*)
  distr_follows :: "('a,'b) distr_d program set"
  where "distr_follows =
         Increasing distr.In Int Increasing distr.iIn Int
         Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
         guarantees
         (\<Inter>i \<in> lessThan Nclients.
          (sub i o distr.Out) Fols
          (%s. nths (distr.In s)
                       {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"

definition
  distr_allowed_acts :: "('a,'b) distr_d program set"
  where "distr_allowed_acts =
       {D. AllowedActs D = insert Id (\<Union>(Acts ` (preserves distr.Out)))}"

definition
  distr_spec :: "('a,'b) distr_d program set"
  where "distr_spec = distr_follows Int distr_allowed_acts"

(** Single-client allocator specification (required) ***)

definition
  (*spec (18)*)
  alloc_increasing :: "'a allocState_d program set"
  where "alloc_increasing = UNIV guarantees Increasing giv"

definition
  (*spec (19)*)
  alloc_safety :: "'a allocState_d program set"
  where "alloc_safety =
         Increasing rel
         guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"

definition
  (*spec (20)*)
  alloc_progress :: "'a allocState_d program set"
  where "alloc_progress =
         Increasing ask Int Increasing rel Int
         Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
         Int
         (\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)}
                 LeadsTo
                 {s. tokens h \<le> tokens (rel s)})
         guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"

definition
  (*spec: preserves part*)
  alloc_preserves :: "'a allocState_d program set"
  where "alloc_preserves = preserves rel Int
                        preserves ask Int
                        preserves allocState_d.dummy"

definition
  (*environmental constraints*)
  alloc_allowed_acts :: "'a allocState_d program set"
  where "alloc_allowed_acts =
       {F. AllowedActs F = insert Id (\<Union>(Acts ` (preserves giv)))}"

definition
  alloc_spec :: "'a allocState_d program set"
  where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                   alloc_allowed_acts Int alloc_preserves"

locale Merge =
  fixes M :: "('a,'b::order) merge_d program"
  assumes
    Merge_spec:  "M \ merge_spec"

locale Distrib =
  fixes D :: "('a,'b::order) distr_d program"
  assumes
    Distrib_spec:  "D \ distr_spec"

(****
#  {** Network specification ***}

#    {*spec (9.1)*}
#    network_ask :: "'a systemState program set
#       "network_ask == \<Inter>i \<in> lessThan Nclients.
#                           Increasing (ask o sub i o client)
#                           guarantees[ask]
#                           (ask  Fols (ask o sub i o client))"

#    {*spec (9.2)*}
#    network_giv :: "'a systemState program set
#       "network_giv == \<Inter>i \<in> lessThan Nclients.
#                           Increasing giv
#                           guarantees[giv o sub i o client]
#                           ((giv o sub i o client) Fols giv)"

#    {*spec (9.3)*}
#    network_rel :: "'a systemState program set
#       "network_rel == \<Inter>i \<in> lessThan Nclients.
#                           Increasing (rel o sub i o client)
#                           guarantees[rel]
#                           (rel  Fols (rel o sub i o client))"

#    {*spec: preserves part*}
#       network_preserves :: "'a systemState program set
#       "network_preserves == preserves giv  Int
#                             (\<Inter>i \<in> lessThan Nclients.
#                              preserves (funPair rel ask o sub i o client))"

#    network_spec :: "'a systemState program set
#       "network_spec == network_ask Int network_giv Int
#                        network_rel Int network_preserves"

#  {** State mappings **}
#    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
#       "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
#                          in (| giv = giv s,
#                                ask = ask s,
#                                rel = rel s,
#                                client   = cl,
#                                dummy    = xtr|)"

#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
#       "sysOfClient == %(cl,al). (| giv = giv al,
#                                    ask = ask al,
#                                    rel = rel al,
#                                    client   = cl,
#                                    systemState.dummy = allocState_d.dummy al|)"
****)

declare subset_preserves_o [THEN subsetD, intro]
declare funPair_o_distrib [simp]
declare Always_INT_distrib [simp]
declare o_apply [simp del]

subsection\<open>Theorems for Merge\<close>

context Merge
begin

lemma Merge_Allowed:
     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
apply (cut_tac Merge_spec)
apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
                      safety_prop_Acts_iff)
done

lemma M_ok_iff [iff]:
     "M ok G = (G \ preserves merge.Out & G \ preserves merge.iOut &
                     M \<in> Allowed G)"
by (auto simp add: Merge_Allowed ok_iff_Allowed)

lemma Merge_Always_Out_eq_iOut:
     "[| G \ preserves merge.Out; G \ preserves merge.iOut; M \ Allowed G |]
      ==> M \<squnion> G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
apply (cut_tac Merge_spec)
apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
done

lemma Merge_Bounded:
     "[| G \ preserves merge.iOut; G \ preserves merge.Out; M \ Allowed G |]
      ==> M \<squnion> G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
apply (cut_tac Merge_spec)
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
done

lemma Merge_Bag_Follows_lemma:
     "[| G \ preserves merge.iOut; G \ preserves merge.Out; M \ Allowed G |]
  ==> M \<squnion> G \<in> Always
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (merge.Out s)
                                  {k. k < length (iOut s) & iOut s ! k = i})) =
              (bag_of o merge.Out) s}"
apply (rule Always_Compl_Un_eq [THEN iffD1])
apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
apply (rule UNIV_AlwaysI, clarify)
apply (subst bag_of_nths_UN_disjoint [symmetric])
  apply (simp)
apply blast
apply (simp add: set_conv_nth)
apply (subgoal_tac
       "(\i \ lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
       lessThan (length (iOut x))")
apply (simp (no_asm_simp) add: o_def)
apply blast
done

lemma Merge_Bag_Follows:
     "M \ (\i \ lessThan Nclients. Increasing (sub i o merge.In))
          guarantees
             (bag_of o merge.Out) Fols
             (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)"
apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
apply (rule Follows_sum)
apply (cut_tac Merge_spec)
apply (auto simp add: merge_spec_def merge_follows_def o_def)
apply (drule guaranteesD)
  prefer 3
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
done

end

subsection\<open>Theorems for Distributor\<close>

context Distrib
begin

lemma Distr_Increasing_Out:
     "D \ Increasing distr.In Int Increasing distr.iIn Int
          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
          guarantees
          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
apply (cut_tac Distrib_spec)
apply (simp add: distr_spec_def distr_follows_def)
apply clarify
apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
done

lemma Distr_Bag_Follows_lemma:
     "[| G \ preserves distr.Out;
         D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
  ==> D \<squnion> G \<in> Always
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (distr.In s)
                                  {k. k < length (iIn s) & iIn s ! k = i})) =
              bag_of (nths (distr.In s) (lessThan (length (iIn s))))}"
apply (erule Always_Compl_Un_eq [THEN iffD1])
apply (rule UNIV_AlwaysI, clarify)
apply (subst bag_of_nths_UN_disjoint [symmetric])
  apply (simp (no_asm))
apply blast
apply (simp add: set_conv_nth)
apply (subgoal_tac
       "(\i \ lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
        lessThan (length (iIn x))")
apply (simp (no_asm_simp))
apply blast
done

lemma D_ok_iff [iff]:
     "D ok G = (G \ preserves distr.Out & D \ Allowed G)"
apply (cut_tac Distrib_spec)
apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
                      safety_prop_Acts_iff ok_iff_Allowed)
done

lemma Distr_Bag_Follows:
"D \ Increasing distr.In Int Increasing distr.iIn Int
      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
      guarantees
       (\<Inter>i \<in> lessThan Nclients.
        (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
        Fols
        (%s. bag_of (nths (distr.In s) (lessThan (length(distr.iIn s))))))"
apply (rule guaranteesI, clarify)
apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
apply (rule Follows_sum)
apply (cut_tac Distrib_spec)
apply (auto simp add: distr_spec_def distr_follows_def o_def)
apply (drule guaranteesD)
  prefer 3
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
done

end

subsection\<open>Theorems for Allocator\<close>

lemma alloc_refinement_lemma:
     "!!f::nat=>nat. (\i \ lessThan n. {s. f i \ g i s})
      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
apply (induct_tac "n")
apply (auto simp add: lessThan_Suc)
done

lemma alloc_refinement:
"(\i \ lessThan Nclients. Increasing (sub i o allocAsk) Int
                           Increasing (sub i o allocRel))
  Int
  Always {s. \<forall>i. i<Nclients -->
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
  Int
  (\<Inter>i \<in> lessThan Nclients.
   \<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
        LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s})
  \<subseteq>
(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
                           Increasing (sub i o allocRel))
  Int
  Always {s. \<forall>i. i<Nclients -->
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
  Int
  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
         {s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
  LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le>
              (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)})"
apply (auto simp add: ball_conj_distrib)
apply (rename_tac F hf)
apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
apply (subgoal_tac "F \ Increasing (tokens o (sub i o allocRel))")
apply (simp add: Increasing_def o_assoc)
apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
done

end

quality99%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.