Theory Analysis_OCL
theory
Analysis_OCL
imports
Analysis_UML
begin
text ‹\label{ex:employee-analysis:ocl}›
section‹OCL Part: Invariant›
text‹These recursive predicates can be defined conservatively
by greatest fix-point
constructions---automatically. See~\<^cite>‹"brucker.ea:hol-ocl-book:2006" and "brucker:interactive:2007"›
for details. For the purpose of this example, we state them as axioms
here.
\begin{ocl}
context Person
inv label : self .boss <> null implies (self .salary ≤ ((self .boss) .salary))
\end{ocl}
›
definition Person_label⇩i⇩n⇩v :: "Person ⇒ Boolean"
where "Person_label⇩i⇩n⇩v (self) ≡
(self .boss <> null implies (self .salary ≤⇩i⇩n⇩t ((self .boss) .salary)))"
definition Person_label⇩i⇩n⇩v⇩A⇩T⇩p⇩r⇩e :: "Person ⇒ Boolean"
where "Person_label⇩i⇩n⇩v⇩A⇩T⇩p⇩r⇩e (self) ≡
(self .boss@pre <> null implies (self .salary@pre ≤⇩i⇩n⇩t ((self .boss@pre) .salary@pre)))"
definition Person_label⇩g⇩l⇩o⇩b⇩a⇩l⇩i⇩n⇩v :: "Boolean"
where "Person_label⇩g⇩l⇩o⇩b⇩a⇩l⇩i⇩n⇩v ≡ (Person .allInstances()->forAll⇩S⇩e⇩t(x | Person_label⇩i⇩n⇩v (x)) and
(Person .allInstances@pre()->forAll⇩S⇩e⇩t(x | Person_label⇩i⇩n⇩v⇩A⇩T⇩p⇩r⇩e (x))))"
lemma "τ ⊨ δ (X .boss) ⟹ τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(X .boss) ∧
τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(X) "
oops
lemma REC_pre : "τ ⊨ Person_label⇩g⇩l⇩o⇩b⇩a⇩l⇩i⇩n⇩v
⟹ τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(X)
⟹ ∃ REC. τ ⊨ REC(X) ≜ (Person_label⇩i⇩n⇩v (X) and (X .boss <> null implies REC(X .boss)))"
oops
text‹This allows to state a predicate:›
axiomatization inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l :: "Person ⇒ Boolean"
where inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l_def:
"(τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(self)) ⟹
(τ ⊨ (inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l(self) ≜ (self .boss <> null implies
(self .salary ≤⇩i⇩n⇩t ((self .boss) .salary)) and
inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l(self .boss))))"
axiomatization inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e :: "Person ⇒ Boolean"
where inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e_def:
"(τ ⊨ Person .allInstances@pre()->includes⇩S⇩e⇩t(self)) ⟹
(τ ⊨ (inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e(self) ≜ (self .boss@pre <> null implies
(self .salary@pre ≤⇩i⇩n⇩t ((self .boss@pre) .salary@pre)) and
inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e(self .boss@pre))))"
lemma inv_1 :
"(τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(self)) ⟹
(τ ⊨ inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l(self) = ((τ ⊨ (self .boss ≐ null)) ∨
( τ ⊨ (self .boss <> null) ∧
τ ⊨ ((self .salary) ≤⇩i⇩n⇩t (self .boss .salary)) ∧
τ ⊨ (inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l(self .boss))))) "
oops
lemma inv_2 :
"(τ ⊨ Person .allInstances@pre()->includes⇩S⇩e⇩t(self)) ⟹
(τ ⊨ inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e(self)) = ((τ ⊨ (self .boss@pre ≐ null)) ∨
(τ ⊨ (self .boss@pre <> null) ∧
(τ ⊨ (self .boss@pre .salary@pre ≤⇩i⇩n⇩t self .salary@pre)) ∧
(τ ⊨ (inv⇩P⇩e⇩r⇩s⇩o⇩n⇩_⇩l⇩a⇩b⇩e⇩l⇩A⇩T⇩p⇩r⇩e(self .boss@pre)))))"
oops
text‹A very first attempt to characterize the axiomatization by an inductive
definition - this can not be the last word since too weak (should be equality!)›
coinductive inv :: "Person ⇒ (𝔄)st ⇒ bool" where
"(τ ⊨ (δ self)) ⟹ ((τ ⊨ (self .boss ≐ null)) ∨
(τ ⊨ (self .boss <> null) ∧ (τ ⊨ (self .boss .salary ≤⇩i⇩n⇩t self .salary)) ∧
( (inv(self .boss))τ )))
⟹ ( inv self τ)"
section‹OCL Part: The Contract of a Recursive Query›
text‹The original specification of a recursive query :
\begin{ocl}
context Person::contents():Set(Integer)
pre: true
post: result = if self.boss = null
then Set{i}
else self.boss.contents()->including(i)
endif
\end{ocl}›
text‹For the case of recursive queries, we use at present just axiomatizations:›
axiomatization contents :: "Person ⇒ Set_Integer" ("(1(_).contents'('))" 50)
where contents_def:
"(self .contents()) = (λ τ. SOME res. let res = λ _. res in
if τ ⊨ (δ self)
then ((τ ⊨ true) ∧
(τ ⊨ res ≜ if (self .boss ≐ null)
then (Set{self .salary})
else (self .boss .contents()
->including⇩S⇩e⇩t(self .salary))
endif))
else τ ⊨ res ≜ invalid)"
and cp0_contents:"(X .contents()) τ = ((λ_. X τ) .contents()) τ"
interpretation contents : contract0 "contents" "λ self. true"
"λ self res. res ≜ if (self .boss ≐ null)
then (Set{self .salary})
else (self .boss .contents()
->including⇩S⇩e⇩t(self .salary))
endif"
proof (unfold_locales)
show "⋀self τ. true τ = true τ" by auto
next
show "⋀self. ∀σ σ' σ''. ((σ, σ') ⊨ true) = ((σ, σ'') ⊨ true)" by auto
next
show "⋀self. self .contents() ≡
λ τ. SOME res. let res = λ _. res in
if τ ⊨ (δ self)
then ((τ ⊨ true) ∧
(τ ⊨ res ≜ if (self .boss ≐ null)
then (Set{self .salary})
else (self .boss .contents()
->including⇩S⇩e⇩t(self .salary))
endif))
else τ ⊨ res ≜ invalid"
by(auto simp: contents_def )
next
have A:"⋀self τ. ((λ_. self τ) .boss ≐ null) τ = (λ_. (self .boss ≐ null) τ) τ"
by (metis (no_types) StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮)
have B:"⋀self τ. (λ_. Set{(λ_. self τ) .salary} τ) = (λ_. Set{self .salary} τ)"
apply(subst UML_Set.OclIncluding.cp0)
apply(subst (2) UML_Set.OclIncluding.cp0)
apply(subst (2) Analysis_UML.cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴) by simp
have C:"⋀self τ. ((λ_. self τ).boss .contents()->including⇩S⇩e⇩t((λ_. self τ).salary) τ) =
(self .boss .contents() ->including⇩S⇩e⇩t(self .salary) τ)"
apply(subst UML_Set.OclIncluding.cp0) apply(subst (2) UML_Set.OclIncluding.cp0)
apply(subst (2) Analysis_UML.cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴)
apply(subst cp0_contents) apply(subst (2) cp0_contents)
apply(subst (2) cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮) by simp
show "⋀self res τ.
(res ≜ if (self .boss) ≐ null then Set{self .salary}
else self .boss .contents()->including⇩S⇩e⇩t(self .salary) endif) τ =
((λ_. res τ) ≜ if (λ_. self τ) .boss ≐ null then Set{(λ_. self τ) .salary}
else(λ_. self τ) .boss .contents()->including⇩S⇩e⇩t((λ_. self τ) .salary) endif) τ"
apply(subst cp_StrongEq)
apply(subst (2) cp_StrongEq)
apply(subst cp_OclIf)
apply(subst (2)cp_OclIf)
by(simp add: A B C)
qed
text‹Specializing @{thm contents.unfold2}, one gets the following more practical rewrite
rule that is amenable to symbolic evaluation:›
theorem unfold_contents :
assumes "cp E"
and "τ ⊨ δ self"
shows "(τ ⊨ E (self .contents())) =
(τ ⊨ E (if self .boss ≐ null
then Set{self .salary}
else self .boss .contents()->including⇩S⇩e⇩t(self .salary) endif))"
by(rule contents.unfold2[of _ _ _ "λ X. true"], simp_all add: assms)
text‹Since we have only one interpretation function, we need the corresponding
operation on the pre-state:›
consts contentsATpre :: "Person ⇒ Set_Integer" ("(1(_).contents@pre'('))" 50)
axiomatization where contentsATpre_def:
" (self).contents@pre() = (λ τ.
SOME res. let res = λ _. res in
if τ ⊨ (δ self)
then ((τ ⊨ true) ∧
(τ ⊨ (res ≜ if (self).boss@pre ≐ null
then Set{(self).salary@pre}
else (self).boss@pre .contents@pre()
->including⇩S⇩e⇩t(self .salary@pre)
endif)))
else τ ⊨ res ≜ invalid)"
and cp0_contents_at_pre:"(X .contents@pre()) τ = ((λ_. X τ) .contents@pre()) τ"
interpretation contentsATpre : contract0 "contentsATpre" "λ self. true"
"λ self res. res ≜ if (self .boss@pre ≐ null)
then (Set{self .salary@pre})
else (self .boss@pre .contents@pre()
->including⇩S⇩e⇩t(self .salary@pre))
endif"
proof (unfold_locales)
show "⋀self τ. true τ = true τ" by auto
next
show "⋀self. ∀σ σ' σ''. ((σ, σ') ⊨ true) = ((σ, σ'') ⊨ true)" by auto
next
show "⋀self. self .contents@pre() ≡
λτ. SOME res. let res = λ _. res in
if τ ⊨ δ self
then τ ⊨ true ∧
τ ⊨ res ≜ (if self .boss@pre ≐ null then Set{self .salary@pre}
else self .boss@pre .contents@pre()->including⇩S⇩e⇩t(self .salary@pre)
endif)
else τ ⊨ res ≜ invalid"
by(auto simp: contentsATpre_def)
next
have A:"⋀self τ. ((λ_. self τ) .boss@pre ≐ null) τ = (λ_. (self .boss@pre ≐ null) τ) τ"
by (metis StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t_⇩P⇩e⇩r⇩s⇩o⇩n cp_StrictRefEq⇩O⇩b⇩j⇩e⇩c⇩t cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre)
have B:"⋀self τ. (λ_. Set{(λ_. self τ) .salary@pre} τ) = (λ_. Set{self .salary@pre} τ)"
apply(subst UML_Set.OclIncluding.cp0)
apply(subst (2) UML_Set.OclIncluding.cp0)
apply(subst (2) Analysis_UML.cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre) by simp
have C:"⋀self τ. ((λ_. self τ).boss@pre .contents@pre()->including⇩S⇩e⇩t((λ_. self τ).salary@pre) τ) =
(self .boss@pre .contents@pre() ->including⇩S⇩e⇩t(self .salary@pre) τ)"
apply(subst UML_Set.OclIncluding.cp0) apply(subst (2) UML_Set.OclIncluding.cp0)
apply(subst (2) Analysis_UML.cp_dot⇩P⇩e⇩r⇩s⇩o⇩n𝒮𝒜ℒ𝒜ℛ𝒴_at_pre)
apply(subst cp0_contents_at_pre) apply(subst (2) cp0_contents_at_pre)
apply(subst (2) cp_dot⇩P⇩e⇩r⇩s⇩o⇩nℬ𝒪𝒮𝒮_at_pre) by simp
show "⋀self res τ.
(res ≜ if (self .boss@pre) ≐ null then Set{self .salary@pre}
else self .boss@pre .contents@pre()->including⇩S⇩e⇩t(self .salary@pre) endif) τ =
((λ_. res τ) ≜ if (λ_. self τ) .boss@pre ≐ null then Set{(λ_. self τ) .salary@pre}
else(λ_. self τ) .boss@pre .contents@pre()->including⇩S⇩e⇩t((λ_. self τ) .salary@pre) endif) τ"
apply(subst cp_StrongEq)
apply(subst (2) cp_StrongEq)
apply(subst cp_OclIf)
apply(subst (2)cp_OclIf)
by(simp add: A B C)
qed
text‹Again, we derive via @{thm [source] contents.unfold2} a Knaster-Tarski like Fixpoint rule
that is amenable to symbolic evaluation:›
theorem unfold_contentsATpre :
assumes "cp E"
and "τ ⊨ δ self"
shows "(τ ⊨ E (self .contents@pre())) =
(τ ⊨ E (if self .boss@pre ≐ null
then Set{self .salary@pre}
else self .boss@pre .contents@pre()->including⇩S⇩e⇩t(self .salary@pre) endif))"
by(rule contentsATpre.unfold2[of _ _ _ "λ X. true"], simp_all add: assms)
text‹Note that these \inlineocl{@pre} variants on methods are only available on queries, \ie,
operations without side-effect.›
section‹OCL Part: The Contract of a User-defined Method›
text‹
The example specification in high-level OCL input syntax reads as follows:
\begin{ocl}
context Person::insert(x:Integer)
pre: true
post: contents():Set(Integer)
contents() = contents@pre()->including(x)
\end{ocl}
This boils down to:
›
definition insert :: "Person ⇒Integer ⇒ Void" ("(1(_).insert'(_'))" 50)
where "self .insert(x) ≡
(λ τ. SOME res. let res = λ _. res in
if (τ ⊨ (δ self)) ∧ (τ ⊨ υ x)
then (τ ⊨ true ∧
(τ ⊨ ((self).contents() ≜ (self).contents@pre()->including⇩S⇩e⇩t(x))))
else τ ⊨ res ≜ invalid)"
text‹The semantic consequences of this definition were computed inside this locale interpretation:›
interpretation insert : contract1 "insert" "λ self x. true"
"λ self x res. ((self .contents()) ≜
(self .contents@pre()->including⇩S⇩e⇩t(x)))"
apply unfold_locales apply(auto simp:insert_def)
apply(subst cp_StrongEq) apply(subst (2) cp_StrongEq)
apply(subst contents.cp0)
apply(subst UML_Set.OclIncluding.cp0)
apply(subst (2) UML_Set.OclIncluding.cp0)
apply(subst contentsATpre.cp0)
by(simp)
text‹The result of this locale interpretation for our @{term insert} contract is the following
set of properties, which serves as basis for automated deduction on them:
\begin{table}[htbp]
\centering
\begin{tabu}{lX[,c,]}
\toprule
Name & Theorem \\
\midrule
@{thm [source] insert.strict0} & @{thm [display=false] insert.strict0} \\
@{thm [source] insert.nullstrict0} & @{thm [display=false] insert.nullstrict0} \\
@{thm [source] insert.strict1} & @{thm [display=false] insert.strict1} \\
@{thm [source] insert.cp⇩P⇩R⇩E} & @{thm [display=false] insert.cp⇩P⇩R⇩E} \\
@{thm [source] insert.cp⇩P⇩O⇩S⇩T} & @{thm [display=false] insert.cp⇩P⇩O⇩S⇩T} \\
@{thm [source] insert.cp_pre} & @{thm [display=false] insert.cp_pre} \\
@{thm [source] insert.cp_post} & @{thm [display=false] insert.cp_post} \\
@{thm [source] insert.cp} & @{thm [display=false] insert.cp} \\
@{thm [source] insert.cp0} & @{thm [display=false] insert.cp0} \\
@{thm [source] insert.def_scheme} & @{thm [display=false] insert.def_scheme} \\
@{thm [source] insert.unfold} & @{thm [display=false] insert.unfold} \\
@{thm [source] insert.unfold2} & @{thm [display=false] insert.unfold2} \\
\bottomrule
\end{tabu}
\caption{Semantic properties resulting from a user-defined operation contract.}
\label{tab:sem_operation_contract}
\end{table}
›
end