Theory VDM_OBJ
theory VDM_OBJ imports OBJ begin
subsection‹Program logic›
text‹\label{sec:ObjLogic}Apart from the addition of proof rules for the three new
instructions, this section is essentially identical to Section
\ref{sec:VDM}.›
subsubsection ‹Assertions and their semantic validity›
text‹Assertions are binary state predicates, as before.›
type_synonym "Assn" = "State ⇒ State ⇒ bool"
definition VDM_validn :: "nat ⇒ OBJ ⇒ Assn ⇒ bool"
(" ⊨⇩_ _ : _ " 50)
where "(⊨⇩n c : A) = (∀ m . m ≤ n ⟶ (∀ s t . (s,c →⇩m t) ⟶ A s t))"
definition VDM_valid :: "OBJ ⇒ Assn ⇒ bool"
(" ⊨ _ : _ " 50)
where "(⊨ c : A) = (∀ s t . (s,c ⇓ t) ⟶ A s t)"
lemma VDM_valid_validn: "⊨ c:A ⟹ ⊨⇩n c:A"
by (simp add: VDM_valid_def VDM_validn_def Sem_def, fastforce)
lemma VDM_validn_valid: "(∀ n . ⊨⇩n c:A) ⟹ ⊨ c:A"
by (simp add: VDM_valid_def VDM_validn_def Sem_def, fastforce)
lemma VDM_lowerm: "⟦ ⊨⇩n c:A; m < n ⟧ ⟹ ⊨⇩m c:A"
apply (simp add: VDM_validn_def, clarsimp)
apply (erule_tac x="ma" in allE, simp)
done
definition Ctxt_validn :: "nat ⇒ (Assn set) ⇒ bool"
(" ⊨⇩_ _ " 50)
where "(⊨⇩n G) = (∀ m . m ≤ n ⟶ (∀ A. A ∈ G ⟶ ⊨⇩n Call : A))"
definition Ctxt_valid :: "Assn set ⇒ bool" (" ⊨ _ " 50)
where "(⊨ G) = (∀ A . A ∈ G ⟶ ⊨ Call : A)"
lemma Ctxt_valid_validn: "⊨ G ⟹ ⊨⇩n G"
apply (simp add: Ctxt_valid_def Ctxt_validn_def, clarsimp)
apply (rule VDM_valid_validn) apply fast
done
lemma Ctxt_validn_valid: "(∀ n . ⊨⇩n G) ⟹ ⊨ G"
apply (simp add: Ctxt_valid_def Ctxt_validn_def, clarsimp)
apply (rule VDM_validn_valid) apply fast
done
lemma Ctxt_lowerm: "⟦ ⊨⇩n G; m < n ⟧ ⟹ ⊨⇩m G"
apply (simp add: Ctxt_validn_def, clarsimp)
apply (rule VDM_lowerm) prefer 2 apply assumption apply fast
done
definition valid :: "(Assn set) ⇒ OBJ ⇒ Assn ⇒ bool"
("_ ⊨ _ : _ " 50)
where "(G ⊨ c : A) = (Ctxt_valid G ⟶ VDM_valid c A)"
definition validn :: "(Assn set) ⇒ nat ⇒ OBJ ⇒ Assn ⇒ bool"
("_ ⊨⇩_ _ : _" 50)
where "(G ⊨⇩n c : A) = (⊨⇩n G ⟶ ⊨⇩n c : A)"
lemma validn_valid: "(∀ n . G ⊨⇩n c : A) ⟹ G ⊨ c : A"
apply (simp add: valid_def validn_def, clarsimp)
apply (rule VDM_validn_valid, clarsimp)
apply (erule_tac x=n in allE, erule mp)
apply (erule Ctxt_valid_validn)
done
lemma ctxt_consn: "⟦ ⊨⇩n G; ⊨⇩n Call:A ⟧ ⟹ ⊨⇩n {A} ∪ G"
by (simp add: Ctxt_validn_def)
subsubsection‹Proof system›
inductive_set VDM_proof :: "(Assn set × OBJ × Assn) set"
where
VDMSkip: "(G, Skip, λ s t . t=s):VDM_proof"
| VDMAssign:
"(G, Assign x e,
λ s t . t = (update (fst s) x (evalE e (fst s)), snd s)):VDM_proof"
| VDMNew:
"(G, New x C,
λ s t . ∃ l . l ∉ Dom (snd s) ∧
t = (update (fst s) x (RVal (Loc l)),
(l,(C,[])) # (snd s))):VDM_proof"
| VDMGet:
"(G, Get x y F,
λ s t . ∃ l C Flds v. (fst s) y = RVal(Loc l) ∧
lookup (snd s) l = Some(C,Flds) ∧
lookup Flds F = Some v ∧
t = (update (fst s) x v, snd s)):VDM_proof"
| VDMPut:
"(G, Put x F e,
λ s t . ∃ l C Flds. (fst s) x = RVal(Loc l) ∧
lookup (snd s) l = Some(C,Flds) ∧
t = (fst s,
(l,(C,(F,evalE e (fst s)) # Flds))
# (snd s))):VDM_proof"
| VDMComp:
"⟦ (G, c, A):VDM_proof; (G, d, B):VDM_proof⟧ ⟹
(G, Comp c d, λ s t . ∃ r . A s r ∧ B r t):VDM_proof"
| VDMIff:
"⟦ (G, c, A):VDM_proof; (G, d, B):VDM_proof⟧ ⟹
(G, Iff b c d,
λ s t . (((evalB b (fst s)) ⟶ A s t) ∧
((¬ (evalB b (fst s))) ⟶ B s t))):VDM_proof"
| VDMWhile:
"⟦ (G,c,B):VDM_proof;
∀ s . (¬ evalB b (fst s)) ⟶ A s s;
∀ s r t. evalB b (fst s) ⟶ B s r ⟶ A r t ⟶ A s t ⟧
⟹ (G, While b c, λ s t . A s t ∧ ¬ (evalB b (fst t))):VDM_proof"
| VDMCall:
"({A} ∪ G, body, A):VDM_proof ⟹ (G, Call, A):VDM_proof"
| VDMAx: "A ∈ G ⟹ (G, Call, A):VDM_proof"
| VDMConseq:
"⟦ (G, c,A):VDM_proof; ∀ s t. A s t ⟶ B s t⟧ ⟹
(G, c, B):VDM_proof"
abbreviation VDM_deriv :: "[Assn set, OBJ, Assn] ⇒ bool"
("_ ⊳ _ : _" [100,100] 50)
where "G ⊳ c : A == (G,c,A) ∈ VDM_proof"
text‹The while-rule is in fact inter-derivable with the following rule.›
lemma Hoare_While:
"G ⊳ c : (λ s t . ∀ r . evalB b (fst s) ⟶ I s r ⟶ I t r) ⟹
G ⊳ While b c : (λ s t. ∀ r . I s r ⟶ (I t r ∧ ¬ evalB b (fst t)))"
apply (subgoal_tac "G ⊳ (While b c) :
(λ s t . (λ s t . ∀r. I s r ⟶ I t r) s t ∧ ¬ (evalB b (fst t)))")
apply (erule VDMConseq)
apply simp
apply (rule VDMWhile) apply assumption apply simp apply simp
done
text‹Here's the proof in the opposite direction.›
lemma VDMWhile_derivable:
"⟦ G ⊳ c : B; ∀ s . (¬ evalB b (fst s)) ⟶ A s s;
∀ s r t. evalB b (fst s) ⟶ B s r ⟶ A r t ⟶ A s t ⟧
⟹ G ⊳ (While b c) : (λ s t . A s t ∧ ¬ (evalB b (fst t)))"
apply (rule VDMConseq)
apply (rule Hoare_While [of G c b "λ s r . ∀ t . A s t ⟶ A r t"])
apply (erule VDMConseq) apply clarsimp
apply fast
done
subsubsection‹Soundness›
lemma MAX:"Suc (max k m) ≤ n ⟹ k ≤ n ∧ m ≤ n"
by (simp add: max_def, case_tac "k ≤ m", simp+)
text‹The following auxiliary lemma for loops is proven by induction
on $n$.›
lemma SoundWhile[rule_format]:
"(∀n. G ⊨⇩n c : B)
⟶ (∀s. (¬ evalB b (fst s)) ⟶ A s s)
⟶ (∀s. evalB b (fst s)
⟶ (∀r. B s r ⟶ (∀t. A r t ⟶ A s t)))
⟶ G ⊨⇩n (While b c) : (λs t. A s t ∧ ¬ evalB b (fst t))"
apply (induct n)
apply clarsimp apply (simp add: validn_def VDM_validn_def, clarsimp)
apply (drule Sem_no_zero_height_derivs) apply simp
apply clarsimp apply (simp add: validn_def VDM_validn_def, clarsimp)
apply (erule Sem_eval_cases)
prefer 2 apply clarsimp
apply clarsimp
apply (erule_tac x=n in allE, erule impE) apply (erule Ctxt_lowerm) apply simp
apply (rotate_tac -1)
apply (erule_tac x=ma in allE, clarsimp)
apply(erule impE) apply (erule Ctxt_lowerm) apply simp
apply (erule_tac x=na in allE, clarsimp) apply fast
done
lemma SoundCall[rule_format]:
"⟦∀n. ⊨⇩n ({A} ∪ G) ⟶ ⊨⇩n body : A⟧ ⟹ ⊨⇩n G ⟶ ⊨⇩n Call : A"
apply (induct_tac n)
apply (simp add: VDM_validn_def, clarsimp)
apply (drule Sem_no_zero_height_derivs) apply simp
apply clarsimp
apply (drule Ctxt_lowerm) apply (subgoal_tac "n < Suc n", assumption) apply simp apply clarsimp
apply (drule ctxt_consn) apply assumption
apply (simp add: VDM_validn_def, clarsimp)
apply (erule Sem_eval_cases, clarsimp)
done
lemma VDM_Sound_n: "G ⊳ c: A ⟹ (∀ n. G ⊨⇩n c:A)"
apply (erule VDM_proof.induct)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, clarsimp)
apply (drule MAX, clarsimp)
apply (erule_tac x=n in allE, clarsimp, rotate_tac -1, erule_tac x=na in allE, clarsimp)
apply (erule_tac x=n in allE, clarsimp, rotate_tac -1, erule_tac x=ma in allE, clarsimp)
apply (rule_tac x=ab in exI, rule_tac x=bb in exI, fast)
apply (simp add: validn_def VDM_validn_def)
apply(clarsimp, erule Sem_eval_cases, clarsimp)
apply (erule thin_rl, rotate_tac 1, erule thin_rl, erule thin_rl)
apply (erule_tac x=n in allE, clarsimp, erule_tac x=na in allE, clarsimp)
apply (erule thin_rl, erule thin_rl)
apply (erule_tac x=n in allE, clarsimp, erule_tac x=na in allE, clarsimp)
apply clarsimp
apply (rule SoundWhile) apply fast
apply (case_tac s, clarsimp)
apply (case_tac s, clarsimp)
apply (simp add: validn_def, clarsimp)
apply (rule SoundCall) prefer 2 apply assumption apply fastforce
apply (simp add: Ctxt_validn_def validn_def) apply fast
apply (simp add: validn_def VDM_validn_def)
done
theorem VDM_Sound: "G ⊳ c: A ⟹ G ⊨ c:A"
by (drule VDM_Sound_n, erule validn_valid)
text‹A simple corollary is soundness w.r.t.~an empty context.›
lemma VDM_Sound_emptyCtxt:"{} ⊳ c : A ⟹ ⊨ c : A"
apply (drule VDM_Sound)
apply (simp add: valid_def, erule mp)
apply (simp add: Ctxt_valid_def)
done
subsubsection‹Derived rules›
lemma WEAK[rule_format]:
"G ⊳ c : A ⟹ (∀ H . G ⊆ H ⟶ H ⊳ c :A)"
apply (erule VDM_proof.induct)
apply clarsimp apply (rule VDMSkip)
apply clarsimp apply (rule VDMAssign)
apply clarsimp apply (rule VDMNew)
apply (rule, rule) apply (rule VDMGet)
apply (rule, rule) apply (rule VDMPut)
apply (rule, rule) apply (rule VDMComp) apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp)
apply (rule,rule) apply (rule VDMIff) apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp)
apply (rule,rule) apply (rule VDMWhile) apply (erule_tac x=H in allE, simp) apply (assumption) apply simp
apply (rule,rule) apply (rule VDMCall) apply (erule_tac x="({A} ∪ H)" in allE, simp) apply fast
apply (rule,rule) apply (rule VDMAx) apply fast
apply (rule,rule) apply (rule VDMConseq) apply (erule_tac x=H in allE, clarsimp) apply assumption apply assumption
done
lemma CutAux:
"(H ⊳ c : A) ⟹
(∀ G P D . (H = (insert P D) ⟶ G ⊳ Call :P ⟶ (G ⊆ D)
⟶ D ⊳ c:A))"
apply (erule VDM_proof.induct)
apply clarify
apply (fast intro: VDMSkip)
apply (fast intro: VDMAssign)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule VDMNew)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule VDMGet)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule VDMPut)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (erule_tac x=Ga in allE) apply (erule_tac x=Ga in allE)
apply (erule_tac x=P in allE) apply (erule_tac x=P in allE)
apply (erule_tac x=D in allE, erule impE, assumption)
apply (erule_tac x=D in allE, erule impE, assumption)
apply (rule VDMComp) apply simp apply simp
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (erule_tac x=Ga in allE) apply (erule_tac x=Ga in allE)
apply (erule_tac x=P in allE) apply (erule_tac x=P in allE)
apply (erule_tac x=D in allE, erule impE, assumption)
apply (erule_tac x=D in allE, erule impE, assumption)
apply (rule VDMIff) apply simp apply simp
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (erule_tac x=Ga in allE)
apply (erule_tac x=P in allE)
apply (erule_tac x=D in allE, erule impE, assumption)
apply (rule VDMWhile) apply simp apply simp
apply simp
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (erule_tac x=Ga in allE)
apply (erule_tac x=P in allE)
apply (erule_tac x="insert A D" in allE, erule impE, simp)
apply (rule VDMCall) apply fastforce
apply clarsimp
apply (erule disjE)
apply clarsimp apply (erule WEAK) apply assumption
apply (erule VDMAx)
apply clarsimp
apply (subgoal_tac "D ⊳ c : A")
apply (erule VDMConseq) apply simp
apply simp
done
lemma Cut:"⟦ G ⊳ Call : P ; (insert P G) ⊳ c : A ⟧ ⟹ G ⊳ c : A"
by (drule CutAux , simp)
definition verified::"Assn set ⇒ bool"
where "verified G = (∀ A . A:G ⟶ G ⊳ body : A)"
lemma verified_preserved: "⟦verified G; A:G⟧ ⟹ verified (G - {A})"
apply (simp add: verified_def, (rule allI)+, rule)
apply (subgoal_tac "(G - {A}) ⊳ Call:A")
apply (subgoal_tac "G = insert A (G - {A})") prefer 2 apply fast
apply (erule_tac x=Aa in allE)
apply (erule impE, simp)
apply (erule Cut) apply simp
apply (erule_tac x=A in allE, clarsimp)
apply (rule VDMCall) apply simp apply (erule WEAK) apply fast
done
lemma SetNonSingleton:
"⟦G ≠ {A}; A ∈ G⟧ ⟹ ∃B. B ≠ A ∧ B ∈ G"
by auto
lemma MutrecAux[rule_format]:
"∀ G . ((finite G ∧ card G = n ∧ verified G ∧ A : G) ⟶ {} ⊳ Call:A)"
apply (induct n)
apply clarsimp
apply clarsimp
apply (case_tac "G = {A}")
apply clarsimp
apply (erule_tac x="{A}" in allE)
apply (clarsimp, simp add:verified_def)
apply (rule VDMCall, clarsimp)
apply (drule SetNonSingleton, assumption)
apply clarsimp
apply (subgoal_tac "(G - {B}) ⊳ Call : B")
apply (erule_tac x="G - {B}" in allE)
apply (erule impE) apply (simp add: verified_preserved)
apply (erule impE) apply (simp add: card_Diff_singleton)
apply simp
apply (simp add: verified_def)
apply (rotate_tac 3) apply (erule_tac x=B in allE, simp)
apply (rule VDMCall) apply simp apply (erule WEAK) apply fast
done
theorem Mutrec:
"⟦ finite G; card G = n; verified G; A : G ⟧ ⟹ {} ⊳ Call:A"
by (rule MutrecAux, fast)
subsubsection‹Completeness›
definition SSpec::"OBJ ⇒ Assn"
where "SSpec c s t = (s,c ⇓ t)"
lemma SSpec_valid: "⊨ c : (SSpec c)"
by (simp add: VDM_valid_def SSpec_def)
lemma SSpec_strong: "⊨ c :A ⟹ ∀ s t . SSpec c s t ⟶ A s t"
by (simp add: VDM_valid_def SSpec_def)
lemma SSpec_derivable:"G ⊳ Call : SSpec Call ⟹ G ⊳ c : SSpec c"
apply (induct c)
apply (rule VDMConseq)
apply (rule VDMSkip) apply (simp add: SSpec_def Sem_def, rule, rule, rule) apply (rule SemSkip) apply simp
apply (rule VDMConseq)
apply (rule VDMAssign) apply (simp add: SSpec_def Sem_def, rule, rule, rule) apply (rule SemAssign) apply simp
apply (rule VDMConseq)
apply (rule VDMNew) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
apply (erule exE, erule conjE)
apply (rule SemNew) apply assumption apply assumption
apply (rule VDMConseq)
apply (rule VDMGet) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply (rule SemGet) apply assumption apply assumption apply assumption apply assumption
apply (rule VDMConseq)
apply (rule VDMPut) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply (rule SemPut) apply assumption apply assumption apply assumption
apply clarsimp
apply (rule VDMConseq)
apply (rule VDMComp) apply assumption+ apply (simp add: SSpec_def Sem_def, clarsimp)
apply rule apply (rule SemComp) apply assumption+ apply simp
apply clarsimp
apply (rule VDMConseq)
apply (erule VDMWhile)
prefer 3
apply (rename_tac BExpr c)
apply (subgoal_tac "∀s t. SSpec (While BExpr c) s t ∧ ¬ evalB BExpr (fst t) ⟶ SSpec (While BExpr c) s t", assumption)
apply simp
apply (simp only: SSpec_def Sem_def) apply (rule, rule, rule) apply (erule SemWhileF) apply simp
apply (simp only: SSpec_def Sem_def) apply (rule, rule, rule)
apply (rule, rule, rule) apply (erule exE)+ apply (rule, erule SemWhileT) apply assumption+ apply simp
apply clarsimp
apply (rule VDMConseq)
apply (rule VDMIff) apply assumption+ apply (simp only: SSpec_def Sem_def)
apply (erule thin_rl, erule thin_rl)
apply (rule, rule, rule)
apply (erule conjE)
apply (rename_tac BExpr c1 c2 s t)
apply (case_tac "evalB BExpr (fst s)")
apply (erule impE, assumption) apply (erule exE) apply (rule, rule SemTrue) apply assumption+
apply (rotate_tac 2, erule impE, assumption) apply (erule exE) apply (rule, rule SemFalse) apply assumption+
done
definition StrongG :: "Assn set"
where "StrongG = {SSpec Call}"
lemma StrongG_Body: "StrongG ⊳ body : SSpec Call"
apply (subgoal_tac "StrongG ⊳ body : SSpec body")
apply (erule VDMConseq) apply (simp add: SSpec_def Sem_def, clarsimp)
apply (rule, erule SemCall)
apply (rule SSpec_derivable) apply (rule VDMAx) apply (simp add: StrongG_def)
done
lemma StrongG_verified: "verified StrongG"
apply (simp add: verified_def)
apply (rule allI)+
apply rule
apply (subgoal_tac "StrongG ⊳ body : SSpec Call")
apply (simp add: StrongG_def)
apply (rule StrongG_Body)
done
lemma SSpec_derivable_empty:"{} ⊳ c : SSpec c"
apply (rule Cut)
apply (rule Mutrec) apply (subgoal_tac "finite StrongG", assumption)
apply (simp add: StrongG_def)
apply (simp add: StrongG_def)
apply (rule StrongG_verified)
apply (simp add: StrongG_def)
apply (rule SSpec_derivable) apply (rule VDMAx) apply simp
done
theorem VDM_Complete: "⊨ c : A ⟹ {} ⊳ c : A"
apply (rule VDMConseq)
apply (rule SSpec_derivable_empty)
apply (erule SSpec_strong)
done
lemma Ctxt_valid_verified: "⊨ G ⟹ verified G"
apply (simp add: Ctxt_valid_def verified_def, clarsimp)
apply (erule_tac x=A in allE, simp)
apply (subgoal_tac "⊨ body : A")
apply (rotate_tac 1, erule thin_rl, drule VDM_Complete) apply (erule WEAK) apply fast
apply (simp only: VDM_valid_def Sem_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule_tac x=s in allE, erule_tac x=t in allE, erule mp)
apply (rule, erule SemCall)
done
lemma Ctxt_verified_valid: "⟦verified G; finite G⟧ ⟹ ⊨ G"
apply (subgoal_tac "(∀ A . A:G ⟶ G ⊳ body : A)")
prefer 2 apply (simp add: verified_def)
apply (simp add: Ctxt_valid_def, clarsimp)
apply (erule_tac x=A in allE, simp)
apply (rule VDM_Sound_emptyCtxt)
apply (rule Mutrec, assumption)
apply (insert card_def) apply fast
apply assumption
apply assumption
done
text‹End of theory VDM_Obj›
end