Up to index of Isabelle/HOL/HoareParallel
theory Gar_Collheader {* \section{The Single Mutator Case} *} theory Gar_Coll imports Graph OG_Syntax begin declare psubsetE [rule del] text {* Declaration of variables: *} record gar_coll_state = M :: nodes E :: edges bc :: "nat set" obc :: "nat set" Ma :: nodes ind :: nat k :: nat z :: bool subsection {* The Mutator *} text {* The mutator first redirects an arbitrary edge @{text "R"} from an arbitrary accessible node towards an arbitrary accessible node @{text "T"}. It then colors the new target @{text "T"} black. We declare the arbitrarily selected node and edge as constants:*} consts R :: nat T :: nat text {* \noindent The following predicate states, given a list of nodes @{text "m"} and a list of edges @{text "e"}, the conditions under which the selected edge @{text "R"} and node @{text "T"} are valid: *} constdefs Mut_init :: "gar_coll_state => bool" "Mut_init ≡ « T ∈ Reach ´E ∧ R < length ´E ∧ T < length ´M »" text {* \noindent For the mutator we consider two modules, one for each action. An auxiliary variable @{text "´z"} is set to false if the mutator has already redirected an edge but has not yet colored the new target. *} constdefs Redirect_Edge :: "gar_coll_state ann_com" "Redirect_Edge ≡ .{´Mut_init ∧ ´z}. 〈´E:=´E[R:=(fst(´E!R), T)],, ´z:= (¬´z)〉" Color_Target :: "gar_coll_state ann_com" "Color_Target ≡ .{´Mut_init ∧ ¬´z}. 〈´M:=´M[T:=Black],, ´z:= (¬´z)〉" Mutator :: "gar_coll_state ann_com" "Mutator ≡ .{´Mut_init ∧ ´z}. WHILE True INV .{´Mut_init ∧ ´z}. DO Redirect_Edge ;; Color_Target OD" subsubsection {* Correctness of the mutator *} lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def lemma Redirect_Edge: "\<turnstile> Redirect_Edge pre(Color_Target)" apply (unfold mutator_defs) apply annhoare apply(simp_all) apply(force elim:Graph2) done lemma Color_Target: "\<turnstile> Color_Target .{´Mut_init ∧ ´z}." apply (unfold mutator_defs) apply annhoare apply(simp_all) done lemma Mutator: "\<turnstile> Mutator .{False}." apply(unfold Mutator_def) apply annhoare apply(simp_all add:Redirect_Edge Color_Target) apply(simp add:mutator_defs Redirect_Edge_def) done subsection {* The Collector *} text {* \noindent A constant @{text "M_init"} is used to give @{text "´Ma"} a suitable first value, defined as a list of nodes where only the @{text "Roots"} are black. *} consts M_init :: nodes constdefs Proper_M_init :: "gar_coll_state => bool" "Proper_M_init ≡ « Blacks M_init=Roots ∧ length M_init=length ´M »" Proper :: "gar_coll_state => bool" "Proper ≡ « Proper_Roots ´M ∧ Proper_Edges(´M, ´E) ∧ ´Proper_M_init »" Safe :: "gar_coll_state => bool" "Safe ≡ « Reach ´E ⊆ Blacks ´M »" lemmas collector_defs = Proper_M_init_def Proper_def Safe_def subsubsection {* Blackening the roots *} constdefs Blacken_Roots :: " gar_coll_state ann_com" "Blacken_Roots ≡ .{´Proper}. ´ind:=0;; .{´Proper ∧ ´ind=0}. WHILE ´ind<length ´M INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind≤length ´M}. DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M}. IF ´ind∈Roots THEN .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M ∧ ´ind∈Roots}. ´M:=´M[´ind:=Black] FI;; .{´Proper ∧ (∀i<´ind+1. i ∈ Roots --> ´M!i=Black) ∧ ´ind<length ´M}. ´ind:=´ind+1 OD" lemma Blacken_Roots: "\<turnstile> Blacken_Roots .{´Proper ∧ Roots⊆Blacks ´M}." apply (unfold Blacken_Roots_def) apply annhoare apply(simp_all add:collector_defs Graph_defs) apply safe apply(simp_all add:nth_list_update) apply (erule less_SucE) apply simp+ apply force apply force done subsubsection {* Propagating black *} constdefs PBInv :: "gar_coll_state => nat => bool" "PBInv ≡ « λind. ´obc < Blacks ´M ∨ (∀i <ind. ¬BtoW (´E!i, ´M) ∨ (¬´z ∧ i=R ∧ (snd(´E!R)) = T ∧ (∃r. ind ≤ r ∧ r < length ´E ∧ BtoW(´E!r,´M))))»" constdefs Propagate_Black_aux :: "gar_coll_state ann_com" "Propagate_Black_aux ≡ .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M}. ´ind:=0;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´ind=0}. WHILE ´ind<length ´E INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind≤length ´E}. DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E}. IF ´M!(fst (´E!´ind)) = Black THEN .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ ´M!fst(´E!´ind)=Black}. ´M:=´M[snd(´E!´ind):=Black];; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv (´ind + 1) ∧ ´ind<length ´E}. ´ind:=´ind+1 FI OD" lemma Propagate_Black_aux: "\<turnstile> Propagate_Black_aux .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ( ´obc < Blacks ´M ∨ ´Safe)}." apply (unfold Propagate_Black_aux_def PBInv_def collector_defs) apply annhoare apply(simp_all add:Graph6 Graph7 Graph8 Graph12) apply force apply force apply force --{* 4 subgoals left *} apply clarify apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12) apply (erule disjE) apply(rule disjI1) apply(erule Graph13) apply force apply (case_tac "M x ! snd (E x ! ind x)=Black") apply (simp add: Graph10 BtoW_def) apply (rule disjI2) apply clarify apply (erule less_SucE) apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify apply (drule le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)≤r") apply fast apply arith apply fast apply fast apply(rule disjI1) apply(erule subset_psubset_trans) apply(erule Graph11) apply fast --{* 3 subgoals left *} apply force apply force --{* last *} apply clarify apply simp apply(subgoal_tac "ind x = length (E x)") apply (rotate_tac -1) apply (simp (asm_lr)) apply(drule Graph1) apply simp apply clarify apply(erule allE, erule impE, assumption) apply force apply force apply arith done subsubsection {* Refining propagating black *} constdefs Auxk :: "gar_coll_state => bool" "Auxk ≡ «´k<length ´M ∧ (´M!´k≠Black ∨ ¬BtoW(´E!´ind, ´M) ∨ ´obc<Blacks ´M ∨ (¬´z ∧ ´ind=R ∧ snd(´E!R)=T ∧ (∃r. ´ind<r ∧ r<length ´E ∧ BtoW(´E!r, ´M))))»" constdefs Propagate_Black :: " gar_coll_state ann_com" "Propagate_Black ≡ .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M}. ´ind:=0;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´ind=0}. WHILE ´ind<length ´E INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind≤length ´E}. DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E}. IF (´M!(fst (´E!´ind)))=Black THEN .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ (´M!fst(´E!´ind))=Black}. ´k:=(snd(´E!´ind));; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E ∧ (´M!fst(´E!´ind))=Black ∧ ´Auxk}. 〈´M:=´M[´k:=Black],, ´ind:=´ind+1〉 ELSE .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ´PBInv ´ind ∧ ´ind<length ´E}. 〈IF (´M!(fst (´E!´ind)))≠Black THEN ´ind:=´ind+1 FI〉 FI OD" lemma Propagate_Black: "\<turnstile> Propagate_Black .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ ( ´obc < Blacks ´M ∨ ´Safe)}." apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs) apply annhoare apply(simp_all add:Graph6 Graph7 Graph8 Graph12) apply force apply force apply force --{* 5 subgoals left *} apply clarify apply(simp add:BtoW_def Proper_Edges_def) --{* 4 subgoals left *} apply clarify apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12) apply (erule disjE) apply (rule disjI1) apply (erule psubset_subset_trans) apply (erule Graph9) apply (case_tac "M x!k x=Black") apply (case_tac "M x ! snd (E x ! ind x)=Black") apply (simp add: Graph10 BtoW_def) apply (rule disjI2) apply clarify apply (erule less_SucE) apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify apply (drule le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)≤r") apply fast apply arith apply fast apply fast apply (simp add: Graph10 BtoW_def) apply (erule disjE) apply (erule disjI1) apply clarify apply (erule less_SucE) apply force apply simp apply (subgoal_tac "Suc R≤r") apply fast apply arith apply(rule disjI1) apply(erule subset_psubset_trans) apply(erule Graph11) apply fast --{* 3 subgoals left *} apply force --{* 2 subgoals left *} apply clarify apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12) apply (erule disjE) apply fast apply clarify apply (erule less_SucE) apply (erule_tac x=i in allE , erule (1) notE impE) apply simp apply clarify apply (drule le_imp_less_or_eq) apply (erule disjE) apply (subgoal_tac "Suc (ind x)≤r") apply fast apply arith apply (simp add: BtoW_def) apply (simp add: BtoW_def) --{* last *} apply clarify apply simp apply(subgoal_tac "ind x = length (E x)") apply (rotate_tac -1) apply (simp (asm_lr)) apply(drule Graph1) apply simp apply clarify apply(erule allE, erule impE, assumption) apply force apply force apply arith done subsubsection {* Counting black nodes *} constdefs CountInv :: "gar_coll_state => nat => bool" "CountInv ≡ « λind. {i. i<ind ∧ ´Ma!i=Black}⊆´bc »" constdefs Count :: " gar_coll_state ann_com" "Count ≡ .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe) ∧ ´bc={}}. ´ind:=0;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe) ∧ ´bc={} ∧ ´ind=0}. WHILE ´ind<length ´M INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ ´CountInv ´ind ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind≤length ´M}. DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ ´CountInv ´ind ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M}. IF ´M!´ind=Black THEN .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ ´CountInv ´ind ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M ∧ ´M!´ind=Black}. ´bc:=insert ´ind ´bc FI;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ ´CountInv (´ind+1) ∧ ( ´obc < Blacks ´Ma ∨ ´Safe) ∧ ´ind<length ´M}. ´ind:=´ind+1 OD" lemma Count: "\<turnstile> Count .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆´bc ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe)}." apply(unfold Count_def) apply annhoare apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs) apply force apply force apply force apply clarify apply simp apply(fast elim:less_SucE) apply clarify apply simp apply(fast elim:less_SucE) apply force apply force done subsubsection {* Appending garbage nodes to the free list *} consts Append_to_free :: "nat × edges => edges" axioms Append_to_free0: "length (Append_to_free (i, e)) = length e" Append_to_free1: "Proper_Edges (m, e) ==> Proper_Edges (m, Append_to_free(i, e))" Append_to_free2: "i ∉ Reach e ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)" constdefs AppendInv :: "gar_coll_state => nat => bool" "AppendInv ≡ «λind. ∀i<length ´M. ind≤i --> i∈Reach ´E --> ´M!i=Black»" constdefs Append :: " gar_coll_state ann_com" "Append ≡ .{´Proper ∧ Roots⊆Blacks ´M ∧ ´Safe}. ´ind:=0;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´Safe ∧ ´ind=0}. WHILE ´ind<length ´M INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind≤length ´M}. DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M}. IF ´M!´ind=Black THEN .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M ∧ ´M!´ind=Black}. ´M:=´M[´ind:=White] ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind<length ´M ∧ ´ind∉Reach ´E}. ´E:=Append_to_free(´ind,´E) FI;; .{´Proper ∧ ´AppendInv (´ind+1) ∧ ´ind<length ´M}. ´ind:=´ind+1 OD" lemma Append: "\<turnstile> Append .{´Proper}." apply(unfold Append_def AppendInv_def) apply annhoare apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) apply(force simp:Blacks_def nth_list_update) apply force apply force apply(force simp add:Graph_defs) apply force apply clarify apply simp apply(rule conjI) apply (erule Append_to_free1) apply clarify apply (drule_tac n = "i" in Append_to_free2) apply force apply force apply force done subsubsection {* Correctness of the Collector *} constdefs Collector :: " gar_coll_state ann_com" "Collector ≡ .{´Proper}. WHILE True INV .{´Proper}. DO Blacken_Roots;; .{´Proper ∧ Roots⊆Blacks ´M}. ´obc:={};; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={}}. ´bc:=Roots;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots}. ´Ma:=M_init;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots ∧ ´Ma=M_init}. WHILE ´obc≠´bc INV .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆´bc ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ (´obc < Blacks ´Ma ∨ ´Safe)}. DO .{´Proper ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M}. ´obc:=´bc;; Propagate_Black;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ (´obc < Blacks ´M ∨ ´Safe)}. ´Ma:=´M;; .{´Proper ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´Ma ∧ Blacks ´Ma⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧ length ´Ma=length ´M ∧ ( ´obc < Blacks ´Ma ∨ ´Safe)}. ´bc:={};; Count OD;; Append OD" lemma Collector: "\<turnstile> Collector .{False}." apply(unfold Collector_def) apply annhoare apply(simp_all add: Blacken_Roots Propagate_Black Count Append) apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs) apply (force simp add: Proper_Roots_def) apply force apply force apply clarify apply (erule disjE) apply(simp add:psubsetI) apply(force dest:subset_antisym) done subsection {* Interference Freedom *} lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def Propagate_Black_def Count_def Append_def lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def lemmas abbrev = collector_defs mutator_defs Invariants lemma interfree_Blacken_Roots_Redirect_Edge: "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)" apply (unfold modules) apply interfree_aux apply safe apply (simp_all add:Graph6 Graph12 abbrev) done lemma interfree_Redirect_Edge_Blacken_Roots: "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)" apply (unfold modules) apply interfree_aux apply safe apply(simp add:abbrev)+ done lemma interfree_Blacken_Roots_Color_Target: "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)" apply (unfold modules) apply interfree_aux apply safe apply(simp_all add:Graph7 Graph8 nth_list_update abbrev) done lemma interfree_Color_Target_Blacken_Roots: "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)" apply (unfold modules ) apply interfree_aux apply safe apply(simp add:abbrev)+ done lemma interfree_Propagate_Black_Redirect_Edge: "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)" apply (unfold modules ) apply interfree_aux --{* 11 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) apply(clarify, simp add:abbrev Graph6 Graph12) apply(clarify, simp add:abbrev Graph6 Graph12) apply(clarify, simp add:abbrev Graph6 Graph12) apply(erule conjE)+ apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) apply(erule Graph4) apply(simp)+ apply (simp add:BtoW_def) apply (simp add:BtoW_def) apply(rule conjI) apply (force simp add:BtoW_def) apply(erule Graph4) apply simp+ --{* 7 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) apply(erule conjE)+ apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) apply(erule Graph4) apply(simp)+ apply (simp add:BtoW_def) apply (simp add:BtoW_def) apply(rule conjI) apply (force simp add:BtoW_def) apply(erule Graph4) apply simp+ --{* 6 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) apply(erule conjE)+ apply(rule conjI) apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) apply(erule Graph4) apply(simp)+ apply (simp add:BtoW_def) apply (simp add:BtoW_def) apply(rule conjI) apply (force simp add:BtoW_def) apply(erule Graph4) apply simp+ apply(simp add:BtoW_def nth_list_update) apply force --{* 5 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) --{* 4 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) apply(rule conjI) apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) apply(erule Graph4) apply(simp)+ apply (simp add:BtoW_def) apply (simp add:BtoW_def) apply(rule conjI) apply (force simp add:BtoW_def) apply(erule Graph4) apply simp+ apply(rule conjI) apply(simp add:nth_list_update) apply force apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black") apply(force simp add:BtoW_def) apply(case_tac "M x !snd (E x ! ind x)=Black") apply(rule disjI2) apply simp apply (erule Graph5) apply simp+ apply(force simp add:BtoW_def) apply(force simp add:BtoW_def) --{* 3 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) --{* 2 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12) apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym) apply clarify apply(erule Graph4) apply(simp)+ apply (simp add:BtoW_def) apply (simp add:BtoW_def) apply(rule conjI) apply (force simp add:BtoW_def) apply(erule Graph4) apply simp+ done lemma interfree_Redirect_Edge_Propagate_Black: "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev)+ done lemma interfree_Propagate_Black_Color_Target: "interfree_aux (Some Propagate_Black, {}, Some Color_Target)" apply (unfold modules ) apply interfree_aux --{* 11 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+ apply(erule conjE)+ apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, erule allE, erule impE, assumption, erule impE, assumption, simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) --{* 7 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) apply(erule conjE)+ apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, erule allE, erule impE, assumption, erule impE, assumption, simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) --{* 6 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) apply clarify apply (rule conjI) apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, erule allE, erule impE, assumption, erule impE, assumption, simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) apply(simp add:nth_list_update) --{* 5 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) --{* 4 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) apply (rule conjI) apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, erule allE, erule impE, assumption, erule impE, assumption, simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) apply(rule conjI) apply(simp add:nth_list_update) apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10, erule subset_psubset_trans, erule Graph11, force) --{* 3 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) --{* 2 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, erule allE, erule impE, assumption, erule impE, assumption, simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) --{* 3 subgoals left *} apply(simp add:abbrev) done lemma interfree_Color_Target_Propagate_Black: "interfree_aux (Some Color_Target, {}, Some Propagate_Black)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev)+ done lemma interfree_Count_Redirect_Edge: "interfree_aux (Some Count, {}, Some Redirect_Edge)" apply (unfold modules) apply interfree_aux --{* 9 subgoals left *} apply(simp_all add:abbrev Graph6 Graph12) --{* 6 subgoals left *} apply(clarify, simp add:abbrev Graph6 Graph12, erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+ done lemma interfree_Redirect_Edge_Count: "interfree_aux (Some Redirect_Edge, {}, Some Count)" apply (unfold modules ) apply interfree_aux apply(clarify,simp add:abbrev)+ apply(simp add:abbrev) done lemma interfree_Count_Color_Target: "interfree_aux (Some Count, {}, Some Color_Target)" apply (unfold modules ) apply interfree_aux --{* 9 subgoals left *} apply(simp_all add:abbrev Graph7 Graph8 Graph12) --{* 6 subgoals left *} apply(clarify,simp add:abbrev Graph7 Graph8 Graph12, erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+ --{* 2 subgoals left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) apply(rule conjI) apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) apply(simp add:nth_list_update) --{* 1 subgoal left *} apply(clarify, simp add:abbrev Graph7 Graph8 Graph12, erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) done lemma interfree_Color_Target_Count: "interfree_aux (Some Color_Target, {}, Some Count)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev)+ apply(simp add:abbrev) done lemma interfree_Append_Redirect_Edge: "interfree_aux (Some Append, {}, Some Redirect_Edge)" apply (unfold modules ) apply interfree_aux apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12) apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+ done lemma interfree_Redirect_Edge_Append: "interfree_aux (Some Redirect_Edge, {}, Some Append)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev Append_to_free0)+ apply (force simp add: Append_to_free2) apply(clarify, simp add:abbrev Append_to_free0)+ done lemma interfree_Append_Color_Target: "interfree_aux (Some Append, {}, Some Color_Target)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+ apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update) done lemma interfree_Color_Target_Append: "interfree_aux (Some Color_Target, {}, Some Append)" apply (unfold modules ) apply interfree_aux apply(clarify, simp add:abbrev Append_to_free0)+ apply (force simp add: Append_to_free2) apply(clarify,simp add:abbrev Append_to_free0)+ done lemmas collector_mutator_interfree = interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target interfree_Count_Redirect_Edge interfree_Count_Color_Target interfree_Append_Redirect_Edge interfree_Append_Color_Target interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black interfree_Redirect_Edge_Count interfree_Color_Target_Count interfree_Redirect_Edge_Append interfree_Color_Target_Append subsubsection {* Interference freedom Collector-Mutator *} lemma interfree_Collector_Mutator: "interfree_aux (Some Collector, {}, Some Mutator)" apply(unfold Collector_def Mutator_def) apply interfree_aux apply(simp_all add:collector_mutator_interfree) apply(unfold modules collector_defs mutator_defs) apply(tactic {* TRYALL (interfree_aux_tac) *}) --{* 32 subgoals left *} apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) --{* 20 subgoals left *} apply(tactic{* TRYALL Clarify_tac *}) apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) apply(tactic {* TRYALL (etac disjE) *}) apply simp_all apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *}) apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),Force_tac]) *}) apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *}) done subsubsection {* Interference freedom Mutator-Collector *} lemma interfree_Mutator_Collector: "interfree_aux (Some Mutator, {}, Some Collector)" apply(unfold Collector_def Mutator_def) apply interfree_aux apply(simp_all add:collector_mutator_interfree) apply(unfold modules collector_defs mutator_defs) apply(tactic {* TRYALL (interfree_aux_tac) *}) --{* 64 subgoals left *} apply(simp_all add:nth_list_update Invariants Append_to_free0)+ apply(tactic{* TRYALL Clarify_tac *}) --{* 4 subgoals left *} apply force apply(simp add:Append_to_free2) apply force apply(simp add:Append_to_free2) done subsubsection {* The Garbage Collection algorithm *} text {* In total there are 289 verification conditions. *} lemma Gar_Coll: "\<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}. COBEGIN Collector .{False}. \<parallel> Mutator .{False}. COEND .{False}." apply oghoare apply(force simp add: Mutator_def Collector_def modules) apply(rule Collector) apply(rule Mutator) apply(simp add:interfree_Collector_Mutator) apply(simp add:interfree_Mutator_Collector) apply force done end
lemmas mutator_defs:
Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
lemmas mutator_defs:
Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
lemma Redirect_Edge:
\<turnstile> Redirect_Edge pre Color_Target
lemma Color_Target:
\<turnstile> Color_Target .{´Mut_init ∧ ´z}.
lemma Mutator:
\<turnstile> Mutator .{False}.
lemmas collector_defs:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
Safe == %s. Reach (E s) ⊆ Blacks (M s)
lemmas collector_defs:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
Safe == %s. Reach (E s) ⊆ Blacks (M s)
lemma Blacken_Roots:
\<turnstile> Blacken_Roots .{´Proper ∧ Roots ⊆ Blacks ´M}.
lemma Propagate_Black_aux:
\<turnstile> Propagate_Black_aux .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.
lemma Propagate_Black:
\<turnstile> Propagate_Black .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.
lemma Count:
\<turnstile> Count .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ ´bc ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe)}.
lemma Append:
\<turnstile> Append .{´Proper}.
lemma Collector:
\<turnstile> Collector .{False}.
lemmas modules:
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
Blacken_Roots == .{´Proper}. ´ind := 0;; .{´Proper ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. IF ´ind ∈ Roots THEN .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M ∧ ´ind ∈ Roots}. ´M := ´M[´ind := Black] FI;; .{´Proper ∧ (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
Propagate_Black == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´ind = 0}. WHILE ´ind < length ´E INV .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind ≤ length ´E}. DO .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. IF ´M ! fst (´E ! ´ind) = Black THEN .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black}. ´k := snd (´E ! ´ind);; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´Auxk}. 〈´M := ´M[´k := Black],, ´ind := ´ind + 1〉 ELSE .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. 〈IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI〉 FI OD
Count == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {}}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {} ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. IF ´M ! ´ind = Black THEN .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc := insert ´ind ´bc FI;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv (´ind + 1) ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
Append == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M}. IF ´M ! ´ind = Black THEN .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M := ´M[´ind := White] ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E := Append_to_free (´ind, ´E) FI;; .{´Proper ∧ ´AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
lemmas modules:
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
Blacken_Roots == .{´Proper}. ´ind := 0;; .{´Proper ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. IF ´ind ∈ Roots THEN .{´Proper ∧ (∀i<´ind. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M ∧ ´ind ∈ Roots}. ´M := ´M[´ind := Black] FI;; .{´Proper ∧ (∀i<´ind + 1. i ∈ Roots --> ´M ! i = Black) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
Propagate_Black == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´ind = 0}. WHILE ´ind < length ´E INV .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind ≤ length ´E}. DO .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. IF ´M ! fst (´E ! ´ind) = Black THEN .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black}. ´k := snd (´E ! ´ind);; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E ∧ ´M ! fst (´E ! ´ind) = Black ∧ ´Auxk}. 〈´M := ´M[´k := Black],, ´ind := ´ind + 1〉 ELSE .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ ´PBInv ´ind ∧ ´ind < length ´E}. 〈IF ´M ! fst (´E ! ´ind) ≠ Black THEN ´ind := ´ind + 1 FI〉 FI OD
Count == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {}}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´bc = {} ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. IF ´M ! ´ind = Black THEN .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv ´ind ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´bc := insert ´ind ´bc FI;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´obc ⊆ Blacks ´Ma ∧ Blacks ´Ma ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ ´CountInv (´ind + 1) ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
Append == .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe}. ´ind := 0;; .{´Proper ∧ Roots ⊆ Blacks ´M ∧ ´Safe ∧ ´ind = 0}. WHILE ´ind < length ´M INV .{´Proper ∧ ´AppendInv ´ind ∧ ´ind ≤ length ´M}. DO .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M}. IF ´M ! ´ind = Black THEN .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´M ! ´ind = Black}. ´M := ´M[´ind := White] ELSE .{´Proper ∧ ´AppendInv ´ind ∧ ´ind < length ´M ∧ ´ind ∉ Reach ´E}. ´E := Append_to_free (´ind, ´E) FI;; .{´Proper ∧ ´AppendInv (´ind + 1) ∧ ´ind < length ´M}. ´ind := ´ind + 1 OD
lemmas Invariants:
PBInv == %s ind. obc s ⊂ Blacks (M s) ∨ (∀i<ind. ¬ BtoW (E s ! i, M s) ∨ ¬ z s ∧ i = R ∧ snd (E s ! R) = T ∧ (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))
Auxk == %s. k s < length (M s) ∧ (M s ! k s ≠ Black ∨ ¬ BtoW (E s ! ind s, M s) ∨ obc s ⊂ Blacks (M s) ∨ ¬ z s ∧ ind s = R ∧ snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
AppendInv == %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black
lemmas Invariants:
PBInv == %s ind. obc s ⊂ Blacks (M s) ∨ (∀i<ind. ¬ BtoW (E s ! i, M s) ∨ ¬ z s ∧ i = R ∧ snd (E s ! R) = T ∧ (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))
Auxk == %s. k s < length (M s) ∧ (M s ! k s ≠ Black ∨ ¬ BtoW (E s ! ind s, M s) ∨ obc s ⊂ Blacks (M s) ∨ ¬ z s ∧ ind s = R ∧ snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
AppendInv == %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black
lemmas abbrev:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
Safe == %s. Reach (E s) ⊆ Blacks (M s)
Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
PBInv == %s ind. obc s ⊂ Blacks (M s) ∨ (∀i<ind. ¬ BtoW (E s ! i, M s) ∨ ¬ z s ∧ i = R ∧ snd (E s ! R) = T ∧ (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))
Auxk == %s. k s < length (M s) ∧ (M s ! k s ≠ Black ∨ ¬ BtoW (E s ! ind s, M s) ∨ obc s ⊂ Blacks (M s) ∨ ¬ z s ∧ ind s = R ∧ snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
AppendInv == %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black
lemmas abbrev:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s
Safe == %s. Reach (E s) ⊆ Blacks (M s)
Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)
Redirect_Edge == .{´Mut_init ∧ ´z}. 〈´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)〉
Color_Target == .{´Mut_init ∧ ¬ ´z}. 〈´M := ´M[T := Black],, ´z := (¬ ´z)〉
PBInv == %s ind. obc s ⊂ Blacks (M s) ∨ (∀i<ind. ¬ BtoW (E s ! i, M s) ∨ ¬ z s ∧ i = R ∧ snd (E s ! R) = T ∧ (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))
Auxk == %s. k s < length (M s) ∧ (M s ! k s ≠ Black ∨ ¬ BtoW (E s ! ind s, M s) ∨ obc s ⊂ Blacks (M s) ∨ ¬ z s ∧ ind s = R ∧ snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))
CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s
AppendInv == %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black
lemma interfree_Blacken_Roots_Redirect_Edge:
interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)
lemma interfree_Redirect_Edge_Blacken_Roots:
interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)
lemma interfree_Blacken_Roots_Color_Target:
interfree_aux (Some Blacken_Roots, {}, Some Color_Target)
lemma interfree_Color_Target_Blacken_Roots:
interfree_aux (Some Color_Target, {}, Some Blacken_Roots)
lemma interfree_Propagate_Black_Redirect_Edge:
interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)
lemma interfree_Redirect_Edge_Propagate_Black:
interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)
lemma interfree_Propagate_Black_Color_Target:
interfree_aux (Some Propagate_Black, {}, Some Color_Target)
lemma interfree_Color_Target_Propagate_Black:
interfree_aux (Some Color_Target, {}, Some Propagate_Black)
lemma interfree_Count_Redirect_Edge:
interfree_aux (Some Count, {}, Some Redirect_Edge)
lemma interfree_Redirect_Edge_Count:
interfree_aux (Some Redirect_Edge, {}, Some Count)
lemma interfree_Count_Color_Target:
interfree_aux (Some Count, {}, Some Color_Target)
lemma interfree_Color_Target_Count:
interfree_aux (Some Color_Target, {}, Some Count)
lemma interfree_Append_Redirect_Edge:
interfree_aux (Some Append, {}, Some Redirect_Edge)
lemma interfree_Redirect_Edge_Append:
interfree_aux (Some Redirect_Edge, {}, Some Append)
lemma interfree_Append_Color_Target:
interfree_aux (Some Append, {}, Some Color_Target)
lemma interfree_Color_Target_Append:
interfree_aux (Some Color_Target, {}, Some Append)
lemmas collector_mutator_interfree:
interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)
interfree_aux (Some Blacken_Roots, {}, Some Color_Target)
interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)
interfree_aux (Some Propagate_Black, {}, Some Color_Target)
interfree_aux (Some Count, {}, Some Redirect_Edge)
interfree_aux (Some Count, {}, Some Color_Target)
interfree_aux (Some Append, {}, Some Redirect_Edge)
interfree_aux (Some Append, {}, Some Color_Target)
interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)
interfree_aux (Some Color_Target, {}, Some Blacken_Roots)
interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)
interfree_aux (Some Color_Target, {}, Some Propagate_Black)
interfree_aux (Some Redirect_Edge, {}, Some Count)
interfree_aux (Some Color_Target, {}, Some Count)
interfree_aux (Some Redirect_Edge, {}, Some Append)
interfree_aux (Some Color_Target, {}, Some Append)
lemmas collector_mutator_interfree:
interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)
interfree_aux (Some Blacken_Roots, {}, Some Color_Target)
interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)
interfree_aux (Some Propagate_Black, {}, Some Color_Target)
interfree_aux (Some Count, {}, Some Redirect_Edge)
interfree_aux (Some Count, {}, Some Color_Target)
interfree_aux (Some Append, {}, Some Redirect_Edge)
interfree_aux (Some Append, {}, Some Color_Target)
interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)
interfree_aux (Some Color_Target, {}, Some Blacken_Roots)
interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)
interfree_aux (Some Color_Target, {}, Some Propagate_Black)
interfree_aux (Some Redirect_Edge, {}, Some Count)
interfree_aux (Some Color_Target, {}, Some Count)
interfree_aux (Some Redirect_Edge, {}, Some Append)
interfree_aux (Some Color_Target, {}, Some Append)
lemma interfree_Collector_Mutator:
interfree_aux (Some Collector, {}, Some Mutator)
lemma interfree_Mutator_Collector:
interfree_aux (Some Mutator, {}, Some Collector)
lemma Gar_Coll:
\<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}. COBEGIN Collector .{False}. \<parallel> Mutator .{False}. COEND .{False}.