Import of AFP entry for Isabelle 2018.
This commit is contained in:
parent
9b9f422bd3
commit
a5b1b8fe20
|
|
@ -153,7 +153,7 @@ where "OclAsSeq\<^sub>P\<^sub>a\<^sub>i\<^sub>r S = Sequence{S .First(), S .
|
|||
subsection{* Definition: asBag *}
|
||||
|
||||
definition OclAsBag\<^sub>S\<^sub>e\<^sub>q :: "[('\<AA>,'\<alpha>::null)Sequence]\<Rightarrow>('\<AA>,'\<alpha>)Bag" ("(_)->asBag\<^sub>S\<^sub>e\<^sub>q'(')")
|
||||
where "OclAsBag\<^sub>S\<^sub>e\<^sub>q S = (\<lambda>\<tau>. Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>\<lambda>s. if list_ex (op = s) \<lceil>\<lceil>Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil> then 1 else 0\<rfloor>\<rfloor>)"
|
||||
where "OclAsBag\<^sub>S\<^sub>e\<^sub>q S = (\<lambda>\<tau>. Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>\<lambda>s. if list_ex ((=) s) \<lceil>\<lceil>Rep_Sequence\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil> then 1 else 0\<rfloor>\<rfloor>)"
|
||||
|
||||
definition OclAsBag\<^sub>S\<^sub>e\<^sub>t :: "[('\<AA>,'\<alpha>::null)Set]\<Rightarrow>('\<AA>,'\<alpha>)Bag" ("(_)->asBag\<^sub>S\<^sub>e\<^sub>t'(')")
|
||||
where "OclAsBag\<^sub>S\<^sub>e\<^sub>t S = (\<lambda>\<tau>. Abs_Bag\<^sub>b\<^sub>a\<^sub>s\<^sub>e \<lfloor>\<lfloor>\<lambda>s. if s \<in> \<lceil>\<lceil>Rep_Set\<^sub>b\<^sub>a\<^sub>s\<^sub>e (S \<tau>)\<rceil>\<rceil> then 1 else 0\<rfloor>\<rfloor>)"
|
||||
|
|
|
|||
|
|
@ -1063,9 +1063,9 @@ lemmas cp_intro[intro!,simp,code_unfold] =
|
|||
cp_defined[THEN allI[THEN allI[THEN cpI1], of defined]]
|
||||
cp_valid[THEN allI[THEN allI[THEN cpI1], of valid]]
|
||||
cp_OclNot[THEN allI[THEN allI[THEN cpI1], of not]]
|
||||
cp_OclAnd[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "op and"]]
|
||||
cp_OclOr[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "op or"]]
|
||||
cp_OclImplies[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "op implies"]]
|
||||
cp_OclAnd[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(and)"]]
|
||||
cp_OclOr[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(or)"]]
|
||||
cp_OclImplies[THEN allI[THEN allI[THEN allI[THEN cpI2]], of "(implies)"]]
|
||||
cp_StrongEq[THEN allI[THEN allI[THEN allI[THEN cpI2]],
|
||||
of "StrongEq"]]
|
||||
|
||||
|
|
|
|||
|
|
@ -291,11 +291,11 @@ qed
|
|||
|
||||
lemma state_update_vs_allInstances_generic_empty:
|
||||
assumes [simp]: "\<And>a. pre_post (mk a) = a"
|
||||
shows "(mk \<lparr>heap=empty, assocs=A\<rparr>) \<Turnstile> OclAllInstances_generic pre_post Type \<doteq> Set{}"
|
||||
shows "(mk \<lparr>heap=Map.empty, assocs=A\<rparr>) \<Turnstile> OclAllInstances_generic pre_post Type \<doteq> Set{}"
|
||||
proof -
|
||||
have state_update_vs_allInstances_empty:
|
||||
"(OclAllInstances_generic pre_post Type) (mk \<lparr>heap=empty, assocs=A\<rparr>) =
|
||||
Set{} (mk \<lparr>heap=empty, assocs=A\<rparr>)"
|
||||
"(OclAllInstances_generic pre_post Type) (mk \<lparr>heap=Map.empty, assocs=A\<rparr>) =
|
||||
Set{} (mk \<lparr>heap=Map.empty, assocs=A\<rparr>)"
|
||||
by(simp add: OclAllInstances_generic_def mtSet_def)
|
||||
show ?thesis
|
||||
apply(simp only: OclValid_def, subst StrictRefEq\<^sub>S\<^sub>e\<^sub>t.cp0,
|
||||
|
|
@ -511,7 +511,7 @@ shows "is_represented_in_state snd x H \<tau>"
|
|||
by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_post_def]])
|
||||
|
||||
lemma state_update_vs_allInstances_at_post_empty:
|
||||
shows "(\<sigma>, \<lparr>heap=empty, assocs=A\<rparr>) \<Turnstile> Type .allInstances() \<doteq> Set{}"
|
||||
shows "(\<sigma>, \<lparr>heap=Map.empty, assocs=A\<rparr>) \<Turnstile> Type .allInstances() \<doteq> Set{}"
|
||||
unfolding OclAllInstances_at_post_def
|
||||
by(rule state_update_vs_allInstances_generic_empty[OF snd_conv])
|
||||
|
||||
|
|
@ -617,7 +617,7 @@ by(rule represented_generic_objects_in_state[OF A[simplified OclAllInstances_at_
|
|||
|
||||
|
||||
lemma state_update_vs_allInstances_at_pre_empty:
|
||||
shows "(\<lparr>heap=empty, assocs=A\<rparr>, \<sigma>) \<Turnstile> Type .allInstances@pre() \<doteq> Set{}"
|
||||
shows "(\<lparr>heap=Map.empty, assocs=A\<rparr>, \<sigma>) \<Turnstile> Type .allInstances@pre() \<doteq> Set{}"
|
||||
unfolding OclAllInstances_at_pre_def
|
||||
by(rule state_update_vs_allInstances_generic_empty[OF fst_conv])
|
||||
|
||||
|
|
@ -1025,7 +1025,7 @@ section{* Accessors on Object *}
|
|||
subsection{* Definition *}
|
||||
|
||||
definition "select_object mt incl smash deref l = smash (foldl incl mt (map deref l))
|
||||
(* smash returns null with mt in input (in this case, object contains null pointer) *)"
|
||||
\<comment> \<open>smash returns null with \<open>mt\<close> in input (in this case, object contains null pointer)\<close>"
|
||||
|
||||
text{* The continuation @{text f} is usually instantiated with a smashing
|
||||
function which is either the identity @{term id} or, for \inlineocl{0..1} cardinalities
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ definition OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('\
|
|||
where "x +\<^sub>i\<^sub>n\<^sub>t y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> + \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "op +\<^sub>i\<^sub>n\<^sub>t" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> + \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "(+\<^sub>i\<^sub>n\<^sub>t)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> + \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclAdd\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def)
|
||||
|
||||
|
||||
|
|
@ -133,7 +133,7 @@ definition OclMinus\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"(
|
|||
where "x -\<^sub>i\<^sub>n\<^sub>t y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> - \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclMinus\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "op -\<^sub>i\<^sub>n\<^sub>t" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> - \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclMinus\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "(-\<^sub>i\<^sub>n\<^sub>t)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> - \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclMinus\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def)
|
||||
|
||||
|
||||
|
|
@ -141,7 +141,7 @@ definition OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('
|
|||
where "x *\<^sub>i\<^sub>n\<^sub>t y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> * \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau>"
|
||||
interpretation OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "op *\<^sub>i\<^sub>n\<^sub>t" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> * \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> * \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclMult\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def)
|
||||
|
||||
text{* Here is the special case of division, which is defined as invalid for division
|
||||
|
|
@ -163,14 +163,14 @@ definition OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('
|
|||
where "x <\<^sub>i\<^sub>n\<^sub>t y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> < \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "op <\<^sub>i\<^sub>n\<^sub>t" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> < \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "(<\<^sub>i\<^sub>n\<^sub>t)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> < \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclLess\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def)
|
||||
|
||||
definition OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r ::"('\<AA>)Integer \<Rightarrow> ('\<AA>)Integer \<Rightarrow> ('\<AA>)Boolean" (infix "\<le>\<^sub>i\<^sub>n\<^sub>t" 35)
|
||||
where "x \<le>\<^sub>i\<^sub>n\<^sub>t y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> \<le> \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "op \<le>\<^sub>i\<^sub>n\<^sub>t" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> \<le> \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r : profile_bin\<^sub>d_\<^sub>d "(\<le>\<^sub>i\<^sub>n\<^sub>t)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> \<le> \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclLe\<^sub>I\<^sub>n\<^sub>t\<^sub>e\<^sub>g\<^sub>e\<^sub>r_def bot_option_def null_option_def)
|
||||
|
||||
subsubsection{* Basic Properties *}
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ definition OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\<AA>)Real \<Rightarrow>
|
|||
where "x +\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> + \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "op +\<^sub>r\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> + \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "(+\<^sub>r\<^sub>e\<^sub>a\<^sub>l)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> + \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclAdd\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def)
|
||||
|
||||
|
||||
|
|
@ -133,7 +133,7 @@ definition OclMinus\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\<AA>)Real \<Rightarrow
|
|||
where "x -\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> - \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclMinus\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "op -\<^sub>r\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> - \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclMinus\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "(-\<^sub>r\<^sub>e\<^sub>a\<^sub>l)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> - \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclMinus\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def)
|
||||
|
||||
|
||||
|
|
@ -141,7 +141,7 @@ definition OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\<AA>)Real \<Rightarrow>
|
|||
where "x *\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> * \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau>"
|
||||
interpretation OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "op *\<^sub>r\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> * \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> * \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclMult\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def)
|
||||
|
||||
text{* Here is the special case of division, which is defined as invalid for division
|
||||
|
|
@ -164,14 +164,14 @@ definition OclLess\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\<AA>)Real \<Rightarrow>
|
|||
where "x <\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> < \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclLess\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "op <\<^sub>r\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> < \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclLess\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "(<\<^sub>r\<^sub>e\<^sub>a\<^sub>l)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> < \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclLess\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def)
|
||||
|
||||
definition OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l ::"('\<AA>)Real \<Rightarrow> ('\<AA>)Real \<Rightarrow> ('\<AA>)Boolean" (infix "\<le>\<^sub>r\<^sub>e\<^sub>a\<^sub>l" 35)
|
||||
where "x \<le>\<^sub>r\<^sub>e\<^sub>a\<^sub>l y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>\<lceil>\<lceil>x \<tau>\<rceil>\<rceil> \<le> \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "op \<le>\<^sub>r\<^sub>e\<^sub>a\<^sub>l" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> \<le> \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
interpretation OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l : profile_bin\<^sub>d_\<^sub>d "(\<le>\<^sub>r\<^sub>e\<^sub>a\<^sub>l)" "\<lambda> x y. \<lfloor>\<lfloor>\<lceil>\<lceil>x\<rceil>\<rceil> \<le> \<lceil>\<lceil>y\<rceil>\<rceil>\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclLe\<^sub>R\<^sub>e\<^sub>a\<^sub>l_def bot_option_def null_option_def)
|
||||
|
||||
subsubsection{* Basic Properties *}
|
||||
|
|
|
|||
|
|
@ -106,7 +106,7 @@ definition OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g ::"('\<AA>)Str
|
|||
where "x +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g y \<equiv> \<lambda> \<tau>. if (\<delta> x) \<tau> = true \<tau> \<and> (\<delta> y) \<tau> = true \<tau>
|
||||
then \<lfloor>\<lfloor>concat [\<lceil>\<lceil>x \<tau>\<rceil>\<rceil>, \<lceil>\<lceil>y \<tau>\<rceil>\<rceil>]\<rfloor>\<rfloor>
|
||||
else invalid \<tau> "
|
||||
interpretation OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g : profile_bin\<^sub>d_\<^sub>d "op +\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g" "\<lambda> x y. \<lfloor>\<lfloor>concat [\<lceil>\<lceil>x\<rceil>\<rceil>, \<lceil>\<lceil>y\<rceil>\<rceil>]\<rfloor>\<rfloor>"
|
||||
interpretation OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g : profile_bin\<^sub>d_\<^sub>d "(+\<^sub>s\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g)" "\<lambda> x y. \<lfloor>\<lfloor>concat [\<lceil>\<lceil>x\<rceil>\<rceil>, \<lceil>\<lceil>y\<rceil>\<rceil>]\<rfloor>\<rfloor>"
|
||||
by unfold_locales (auto simp:OclAdd\<^sub>S\<^sub>t\<^sub>r\<^sub>i\<^sub>n\<^sub>g_def bot_option_def null_option_def)
|
||||
|
||||
(* TODO : size(), concat, substring(s:string) toInteger, toReal, at(i:Integer), characters() etc. *)
|
||||
|
|
|
|||
|
|
@ -3072,11 +3072,11 @@ lemma StrictRefEq\<^sub>S\<^sub>e\<^sub>t_exec[simp,code_unfold] :
|
|||
(if \<delta> x then (if \<delta> y
|
||||
then ((x->forAll\<^sub>S\<^sub>e\<^sub>t(z| y->includes\<^sub>S\<^sub>e\<^sub>t(z)) and (y->forAll\<^sub>S\<^sub>e\<^sub>t(z| x->includes\<^sub>S\<^sub>e\<^sub>t(z)))))
|
||||
else if \<upsilon> y
|
||||
then false (* x'->includes = null *)
|
||||
then false \<comment> \<open>\<open>x'->includes = null\<close>\<close>
|
||||
else invalid
|
||||
endif
|
||||
endif)
|
||||
else if \<upsilon> x (* null = ??? *)
|
||||
else if \<upsilon> x \<comment> \<open>\<open>null = ???\<close>\<close>
|
||||
then if \<upsilon> y then not(\<delta> y) else invalid endif
|
||||
else invalid
|
||||
endif
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ oops
|
|||
occur in the state. *)
|
||||
|
||||
lemma REC_pre : "\<tau> \<Turnstile> Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>i\<^sub>n\<^sub>v
|
||||
\<Longrightarrow> \<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(X) (* X represented object in state *)
|
||||
\<Longrightarrow> \<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(X) \<comment> \<open>\<open>X\<close> represented object in state\<close>
|
||||
\<Longrightarrow> \<exists> REC. \<tau> \<Turnstile> REC(X) \<triangleq> (Person_label\<^sub>i\<^sub>n\<^sub>v (X) and (X .boss <> null implies REC(X .boss)))"
|
||||
oops (* Attempt to allegiate the burden of he following axiomatizations: could be
|
||||
a witness for a constant specification ...*)
|
||||
|
|
@ -227,8 +227,8 @@ axiomatization where contentsATpre_def:
|
|||
" (self).contents@pre() = (\<lambda> \<tau>.
|
||||
SOME res. let res = \<lambda> _. res in
|
||||
if \<tau> \<Turnstile> (\<delta> self)
|
||||
then ((\<tau> \<Turnstile> true) \<and> (* pre *)
|
||||
(\<tau> \<Turnstile> (res \<triangleq> if (self).boss@pre \<doteq> null (* post *)
|
||||
then ((\<tau> \<Turnstile> true) \<and> \<comment> \<open>pre\<close>
|
||||
(\<tau> \<Turnstile> (res \<triangleq> if (self).boss@pre \<doteq> null \<comment> \<open>post\<close>
|
||||
then Set{(self).salary@pre}
|
||||
else (self).boss@pre .contents@pre()
|
||||
->including\<^sub>S\<^sub>e\<^sub>t(self .salary@pre)
|
||||
|
|
|
|||
|
|
@ -194,7 +194,7 @@ lemmas cps23 =
|
|||
StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_strict2
|
||||
[of "x::Person",
|
||||
simplified StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n[symmetric]]
|
||||
|
||||
for x y \<tau> P Q
|
||||
text{* For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)},
|
||||
a test on the actual type \inlineocl{.oclIsTypeOf($C$)} as well as its relaxed form
|
||||
\inlineocl{.oclIsKindOf($C$)} (corresponding exactly to Java's \verb+instanceof+-operator.
|
||||
|
|
@ -244,7 +244,7 @@ begin
|
|||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> null \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> invalid \<tau> (* down-cast exception *)
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> invalid \<tau> \<comment> \<open>down-cast exception\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid a\<rfloor>\<rfloor>)"
|
||||
end
|
||||
|
||||
|
|
@ -320,7 +320,7 @@ begin
|
|||
"(X::OclAny) .oclIsTypeOf(OclAny) \<equiv>
|
||||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> true \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)"
|
||||
end
|
||||
|
|
@ -328,7 +328,7 @@ end
|
|||
lemma OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny':
|
||||
"(X::OclAny) .oclIsTypeOf(OclAny) =
|
||||
(\<lambda> \<tau>. if \<tau> \<Turnstile> \<upsilon> X then (case X \<tau> of
|
||||
\<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
\<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> true \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)
|
||||
else invalid \<tau>)"
|
||||
|
|
@ -339,7 +339,7 @@ interpretation OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAn
|
|||
profile_mono_schemeV
|
||||
"OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y::OclAny \<Rightarrow> Boolean"
|
||||
"\<lambda> X. (case X of
|
||||
\<lfloor>None\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor> (* invalid ?? *)
|
||||
\<lfloor>None\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid None \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)"
|
||||
apply(unfold_locales, simp add: atomize_eq, rule ext)
|
||||
|
|
@ -352,8 +352,8 @@ begin
|
|||
"(X::Person) .oclIsTypeOf(OclAny) \<equiv>
|
||||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
| \<lfloor>\<lfloor> _ \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)" (* must have actual type Person otherwise *)
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor> _ \<rfloor>\<rfloor> \<Rightarrow> false \<tau>) \<comment> \<open>must have actual type \<open>Person\<close> otherwise\<close>"
|
||||
end
|
||||
|
||||
overloading OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n \<equiv> "OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: OclAny \<Rightarrow> Boolean"
|
||||
|
|
@ -681,8 +681,8 @@ by(rule OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\
|
|||
lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y2:
|
||||
assumes [simp]: "\<And>x. pre_post (x, x) = x"
|
||||
shows "\<exists>\<tau>. (\<tau> \<Turnstile> not ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsTypeOf(OclAny))))"
|
||||
proof - fix oid a let ?t0 = "\<lparr>heap = empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
|
||||
assocs = empty\<rparr>" show ?thesis
|
||||
proof - fix oid a let ?t0 = "\<lparr>heap = Map.empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
|
||||
assocs = Map.empty\<rparr>" show ?thesis
|
||||
apply(rule_tac x = "(?t0, ?t0)" in exI, simp add: OclValid_def del: OclAllInstances_generic_def)
|
||||
apply(simp only: UML_Set.OclForall_def refl if_True
|
||||
OclAllInstances_generic_defined[simplified OclValid_def])
|
||||
|
|
@ -801,8 +801,8 @@ definition eval_extract :: "('\<AA>,('a::object) option option) val
|
|||
\<Rightarrow> (oid \<Rightarrow> ('\<AA>,'c::null) val)
|
||||
\<Rightarrow> ('\<AA>,'c::null) val"
|
||||
where "eval_extract X f = (\<lambda> \<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau> (* exception propagation *)
|
||||
| \<lfloor> \<bottom> \<rfloor> \<Rightarrow> invalid \<tau> (* dereferencing null pointer *)
|
||||
\<bottom> \<Rightarrow> invalid \<tau> \<comment> \<open>exception propagation\<close>
|
||||
| \<lfloor> \<bottom> \<rfloor> \<Rightarrow> invalid \<tau> \<comment> \<open>dereferencing null pointer\<close>
|
||||
| \<lfloor>\<lfloor> obj \<rfloor>\<rfloor> \<Rightarrow> f (oid_of obj) \<tau>)"
|
||||
|
||||
definition "choose\<^sub>2_1 = fst"
|
||||
|
|
@ -1054,30 +1054,30 @@ definition "person9 \<equiv> mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n
|
|||
text_raw{* \endisatagafp*}
|
||||
|
||||
definition
|
||||
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor>))
|
||||
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor>))
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid1 \<lfloor>1200\<rfloor>))
|
||||
(*oid2*)
|
||||
\<^cancel>\<open>oid2\<close>
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid3 \<lfloor>2600\<rfloor>))
|
||||
(oid4 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person5)
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid5 \<lfloor>2300\<rfloor>))
|
||||
(*oid6*)
|
||||
(*oid7*)
|
||||
\<^cancel>\<open>oid6\<close>
|
||||
\<^cancel>\<open>oid7\<close>
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
|
||||
assocs = empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid3],[oid4]],[[oid5],[oid3]]]) \<rparr>"
|
||||
assocs = Map.empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid3],[oid4]],[[oid5],[oid3]]]) \<rparr>"
|
||||
|
||||
definition
|
||||
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
|
||||
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
|
||||
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
|
||||
(*oid4*)
|
||||
\<^cancel>\<open>oid4\<close>
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person6)
|
||||
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
|
||||
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
|
||||
assocs = empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid1],[oid1]],[[oid5],[oid6]],[[oid6],[oid6]]]) \<rparr>"
|
||||
assocs = Map.empty(oid\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> \<mapsto> [[[oid0],[oid1]],[[oid1],[oid1]],[[oid5],[oid6]],[[oid6],[oid6]]]) \<rparr>"
|
||||
|
||||
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = empty, assocs = empty \<rparr>"
|
||||
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = Map.empty, assocs = Map.empty \<rparr>"
|
||||
|
||||
|
||||
lemma basic_\<tau>_wff: "WFF(\<sigma>\<^sub>1,\<sigma>\<^sub>1')"
|
||||
|
|
@ -1087,10 +1087,10 @@ by(auto simp: WFF_def \<sigma>\<^sub>1_def \<sigma>\<^sub>1'_def
|
|||
person1_def person2_def person3_def person4_def
|
||||
person5_def person6_def person7_def person8_def person9_def)
|
||||
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1) = {oid0,oid1,(*,oid2*)oid3,oid4,oid5(*,oid6,oid7*),oid8}"
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1) = {oid0,oid1\<^cancel>\<open>,oid2\<close>,oid3,oid4,oid5\<^cancel>\<open>,oid6,oid7\<close>,oid8}"
|
||||
by(auto simp: \<sigma>\<^sub>1_def)
|
||||
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1') = {oid0,oid1,oid2,oid3,(*,oid4*)oid5,oid6,oid7,oid8}"
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1') = {oid0,oid1,oid2,oid3\<^cancel>\<open>,oid4\<close>,oid5,oid6,oid7,oid8}"
|
||||
by(auto simp: \<sigma>\<^sub>1'_def)
|
||||
|
||||
text_raw{* \isatagafp *}
|
||||
|
|
@ -1238,13 +1238,13 @@ Assert "\<And>s\<^sub>p\<^sub>r\<^sub>e s\<^sub>p\<^sub>o\<^sub>s\<^sub>t. (s\
|
|||
|
||||
lemma \<sigma>_modifiedonly: "(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny)
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)*)}->oclIsModifiedOnly())"
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)\<close>}->oclIsModifiedOnly())"
|
||||
apply(simp add: OclIsModifiedOnly_def OclValid_def
|
||||
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1292,13 +1292,13 @@ proof -
|
|||
show ?thesis
|
||||
apply(rule framing[where X = "Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny)
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)*)}"])
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)\<close>}"])
|
||||
apply(cut_tac \<sigma>_modifiedonly)
|
||||
apply(simp only: OclValid_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1320,12 +1320,12 @@ proof -
|
|||
done
|
||||
qed
|
||||
|
||||
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = empty
|
||||
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = Map.empty
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9)
|
||||
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
|
||||
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person6)
|
||||
(*oid4*)
|
||||
\<^cancel>\<open>oid4\<close>
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
|
||||
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
|
||||
|
|
@ -1349,8 +1349,8 @@ qed
|
|||
declare const_ss [simp]
|
||||
|
||||
lemma "\<And>\<sigma>\<^sub>1.
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Person .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6,
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(Person)(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 })"
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Person .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6,
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(Person)\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 })"
|
||||
apply(subst perm_\<sigma>\<^sub>1')
|
||||
apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1371,7 +1371,7 @@ by(simp_all add: OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_\<AA>
|
|||
lemma "\<And>\<sigma>\<^sub>1.
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (OclAny .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny),
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny),
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny),
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny) })"
|
||||
apply(subst perm_\<sigma>\<^sub>1')
|
||||
apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ oops
|
|||
occur in the state. *)
|
||||
|
||||
lemma REC_pre : "\<tau> \<Turnstile> Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>i\<^sub>n\<^sub>v
|
||||
\<Longrightarrow> \<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(X) (* X represented object in state *)
|
||||
\<Longrightarrow> \<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(X) \<comment> \<open>\<open>X\<close> represented object in state\<close>
|
||||
\<Longrightarrow> \<exists> REC. \<tau> \<Turnstile> REC(X) \<triangleq> (Person_label\<^sub>i\<^sub>n\<^sub>v (X) and (X .boss <> null implies REC(X .boss)))"
|
||||
oops (* Attempt to allegiate the burden of he following axiomatizations: could be
|
||||
a witness for a constant specification ...*)
|
||||
|
|
|
|||
|
|
@ -184,7 +184,7 @@ lemmas cps23 =
|
|||
StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_strict2
|
||||
[of "x::Person",
|
||||
simplified StrictRefEq\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n[symmetric]]
|
||||
|
||||
for x y \<tau> P Q
|
||||
text{* For each Class \emph{C}, we will have a casting operation \inlineocl{.oclAsType($C$)},
|
||||
a test on the actual type \inlineocl{.oclIsTypeOf($C$)} as well as its relaxed form
|
||||
\inlineocl{.oclIsKindOf($C$)} (corresponding exactly to Java's \verb+instanceof+-operator.
|
||||
|
|
@ -234,7 +234,7 @@ begin
|
|||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> null \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> invalid \<tau> (* down-cast exception *)
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> invalid \<tau> \<comment> \<open>down-cast exception\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>(a,b)\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid a b \<rfloor>\<rfloor>)"
|
||||
end
|
||||
|
||||
|
|
@ -309,7 +309,7 @@ begin
|
|||
"(X::OclAny) .oclIsTypeOf(OclAny) \<equiv>
|
||||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> true \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)"
|
||||
end
|
||||
|
|
@ -317,7 +317,7 @@ end
|
|||
lemma OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAny':
|
||||
"(X::OclAny) .oclIsTypeOf(OclAny) =
|
||||
(\<lambda> \<tau>. if \<tau> \<Turnstile> \<upsilon> X then (case X \<tau> of
|
||||
\<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
\<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<bottom> \<rfloor>\<rfloor> \<Rightarrow> true \<tau>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)
|
||||
else invalid \<tau>)"
|
||||
|
|
@ -328,7 +328,7 @@ interpretation OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y_OclAn
|
|||
profile_mono_schemeV
|
||||
"OclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y::OclAny \<Rightarrow> Boolean"
|
||||
"\<lambda> X. (case X of
|
||||
\<lfloor>None\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor> (* invalid ?? *)
|
||||
\<lfloor>None\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid None \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>True\<rfloor>\<rfloor>
|
||||
| \<lfloor>\<lfloor>mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>_\<rfloor> \<rfloor>\<rfloor> \<Rightarrow> \<lfloor>\<lfloor>False\<rfloor>\<rfloor>)"
|
||||
apply(unfold_locales, simp add: atomize_eq, rule ext)
|
||||
|
|
@ -341,8 +341,8 @@ begin
|
|||
"(X::Person) .oclIsTypeOf(OclAny) \<equiv>
|
||||
(\<lambda>\<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau>
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> (* invalid ?? *)
|
||||
| \<lfloor>\<lfloor> _ \<rfloor>\<rfloor> \<Rightarrow> false \<tau>)" (* must have actual type Person otherwise *)
|
||||
| \<lfloor>\<bottom>\<rfloor> \<Rightarrow> true \<tau> \<comment> \<open>invalid ??\<close>
|
||||
| \<lfloor>\<lfloor> _ \<rfloor>\<rfloor> \<Rightarrow> false \<tau>) \<comment> \<open>must have actual type \<open>Person\<close> otherwise\<close>"
|
||||
end
|
||||
|
||||
overloading OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n \<equiv> "OclIsTypeOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n :: OclAny \<Rightarrow> Boolean"
|
||||
|
|
@ -670,8 +670,8 @@ by(rule OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\
|
|||
lemma OclAny_allInstances_generic_oclIsTypeOf\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y2:
|
||||
assumes [simp]: "\<And>x. pre_post (x, x) = x"
|
||||
shows "\<exists>\<tau>. (\<tau> \<Turnstile> not ((OclAllInstances_generic pre_post OclAny)->forAll\<^sub>S\<^sub>e\<^sub>t(X|X .oclIsTypeOf(OclAny))))"
|
||||
proof - fix oid a let ?t0 = "\<lparr>heap = empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
|
||||
assocs = empty\<rparr>" show ?thesis
|
||||
proof - fix oid a let ?t0 = "\<lparr>heap = Map.empty(oid \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y (mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y oid \<lfloor>a\<rfloor>)),
|
||||
assocs = Map.empty\<rparr>" show ?thesis
|
||||
apply(rule_tac x = "(?t0, ?t0)" in exI, simp add: OclValid_def del: OclAllInstances_generic_def)
|
||||
apply(simp only: UML_Set.OclForall_def refl if_True
|
||||
OclAllInstances_generic_defined[simplified OclValid_def])
|
||||
|
|
@ -778,8 +778,8 @@ definition eval_extract :: "('\<AA>,('a::object) option option) val
|
|||
\<Rightarrow> (oid \<Rightarrow> ('\<AA>,'c::null) val)
|
||||
\<Rightarrow> ('\<AA>,'c::null) val"
|
||||
where "eval_extract X f = (\<lambda> \<tau>. case X \<tau> of
|
||||
\<bottom> \<Rightarrow> invalid \<tau> (* exception propagation *)
|
||||
| \<lfloor> \<bottom> \<rfloor> \<Rightarrow> invalid \<tau> (* dereferencing null pointer *)
|
||||
\<bottom> \<Rightarrow> invalid \<tau> \<comment> \<open>exception propagation\<close>
|
||||
| \<lfloor> \<bottom> \<rfloor> \<Rightarrow> invalid \<tau> \<comment> \<open>dereferencing null pointer\<close>
|
||||
| \<lfloor>\<lfloor> obj \<rfloor>\<rfloor> \<Rightarrow> f (oid_of obj) \<tau>)"
|
||||
|
||||
|
||||
|
|
@ -810,7 +810,7 @@ definition "select\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\<A>\<N>\<Y> f
|
|||
|
||||
|
||||
definition "select\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<B>\<O>\<S>\<S> f = (\<lambda> X. case X of
|
||||
(mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n _ _ \<bottom>) \<Rightarrow> null (* object contains null pointer *)
|
||||
(mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n _ _ \<bottom>) \<Rightarrow> null \<comment> \<open>object contains null pointer\<close>
|
||||
| (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n _ _ \<lfloor>boss\<rfloor>) \<Rightarrow> f (\<lambda>x _. \<lfloor>\<lfloor>x\<rfloor>\<rfloor>) boss)"
|
||||
|
||||
|
||||
|
|
@ -1012,30 +1012,30 @@ definition "person8 \<equiv> mk\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y
|
|||
definition "person9 \<equiv> mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid8 \<lfloor>0\<rfloor> None"
|
||||
|
||||
definition
|
||||
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor> \<lfloor>oid1\<rfloor>))
|
||||
"\<sigma>\<^sub>1 \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid0 \<lfloor>1000\<rfloor> \<lfloor>oid1\<rfloor>))
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid1 \<lfloor>1200\<rfloor> None))
|
||||
(*oid2*)
|
||||
\<^cancel>\<open>oid2\<close>
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid3 \<lfloor>2600\<rfloor> \<lfloor>oid4\<rfloor>))
|
||||
(oid4 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person5)
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n (mk\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n oid5 \<lfloor>2300\<rfloor> \<lfloor>oid3\<rfloor>))
|
||||
(*oid6*)
|
||||
(*oid7*)
|
||||
\<^cancel>\<open>oid6\<close>
|
||||
\<^cancel>\<open>oid7\<close>
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
|
||||
assocs = empty \<rparr>"
|
||||
assocs = Map.empty \<rparr>"
|
||||
|
||||
definition
|
||||
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
|
||||
"\<sigma>\<^sub>1' \<equiv> \<lparr> heap = Map.empty(oid0 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person1)
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
|
||||
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
|
||||
(*oid4*)
|
||||
\<^cancel>\<open>oid4\<close>
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person6)
|
||||
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
|
||||
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9),
|
||||
assocs = empty \<rparr>"
|
||||
assocs = Map.empty \<rparr>"
|
||||
|
||||
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = empty, assocs = empty \<rparr>"
|
||||
definition "\<sigma>\<^sub>0 \<equiv> \<lparr> heap = Map.empty, assocs = Map.empty \<rparr>"
|
||||
|
||||
|
||||
lemma basic_\<tau>_wff: "WFF(\<sigma>\<^sub>1,\<sigma>\<^sub>1')"
|
||||
|
|
@ -1045,10 +1045,10 @@ by(auto simp: WFF_def \<sigma>\<^sub>1_def \<sigma>\<^sub>1'_def
|
|||
person1_def person2_def person3_def person4_def
|
||||
person5_def person6_def person7_def person8_def person9_def)
|
||||
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1) = {oid0,oid1,(*,oid2*)oid3,oid4,oid5(*,oid6,oid7*),oid8}"
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1) = {oid0,oid1\<^cancel>\<open>,oid2\<close>,oid3,oid4,oid5\<^cancel>\<open>,oid6,oid7\<close>,oid8}"
|
||||
by(auto simp: \<sigma>\<^sub>1_def)
|
||||
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1') = {oid0,oid1,oid2,oid3,(*,oid4*)oid5,oid6,oid7,oid8}"
|
||||
lemma [simp,code_unfold]: "dom (heap \<sigma>\<^sub>1') = {oid0,oid1,oid2,oid3\<^cancel>\<open>,oid4\<close>,oid5,oid6,oid7,oid8}"
|
||||
by(auto simp: \<sigma>\<^sub>1'_def)
|
||||
|
||||
text_raw{* \isatagafp *}
|
||||
|
|
@ -1191,13 +1191,13 @@ Assert "\<And>s\<^sub>p\<^sub>r\<^sub>e s\<^sub>p\<^sub>o\<^sub>s\<^sub>t. (s\
|
|||
|
||||
lemma \<sigma>_modifiedonly: "(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny)
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)*)}->oclIsModifiedOnly())"
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)\<close>}->oclIsModifiedOnly())"
|
||||
apply(simp add: OclIsModifiedOnly_def OclValid_def
|
||||
oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1245,13 +1245,13 @@ proof -
|
|||
show ?thesis
|
||||
apply(rule framing[where X = "Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny)
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)*)
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5 .oclAsType(OclAny)\<close>
|
||||
, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)*)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)*)}"])
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8 .oclAsType(OclAny)\<close>
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny)\<close>}"])
|
||||
apply(cut_tac \<sigma>_modifiedonly)
|
||||
apply(simp only: OclValid_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1273,12 +1273,12 @@ proof -
|
|||
done
|
||||
qed
|
||||
|
||||
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = empty
|
||||
lemma perm_\<sigma>\<^sub>1' : "\<sigma>\<^sub>1' = \<lparr> heap = Map.empty
|
||||
(oid8 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person9)
|
||||
(oid7 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person8)
|
||||
(oid6 \<mapsto> in\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y person7)
|
||||
(oid5 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person6)
|
||||
(*oid4*)
|
||||
\<^cancel>\<open>oid4\<close>
|
||||
(oid3 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person4)
|
||||
(oid2 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person3)
|
||||
(oid1 \<mapsto> in\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n person2)
|
||||
|
|
@ -1302,8 +1302,8 @@ qed
|
|||
declare const_ss [simp]
|
||||
|
||||
lemma "\<And>\<sigma>\<^sub>1.
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Person .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6,
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(Person)(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 })"
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (Person .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6,
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7 .oclAsType(Person)\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 })"
|
||||
apply(subst perm_\<sigma>\<^sub>1')
|
||||
apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3_def X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4_def
|
||||
|
|
@ -1324,7 +1324,7 @@ by(simp_all add: OclAsType\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_\<AA>
|
|||
lemma "\<And>\<sigma>\<^sub>1.
|
||||
(\<sigma>\<^sub>1,\<sigma>\<^sub>1') \<Turnstile> (OclAny .allInstances() \<doteq> Set{ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 .oclAsType(OclAny), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 .oclAsType(OclAny),
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 .oclAsType(OclAny), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n4 .oclAsType(OclAny)
|
||||
(*, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5*), X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny),
|
||||
\<^cancel>\<open>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n5\<close>, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n6 .oclAsType(OclAny),
|
||||
X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n7, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n8, X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n9 .oclAsType(OclAny) })"
|
||||
apply(subst perm_\<sigma>\<^sub>1')
|
||||
apply(simp only: oid0_def oid1_def oid2_def oid3_def oid4_def oid5_def oid6_def oid7_def oid8_def
|
||||
|
|
|
|||
Loading…
Reference in New Issue