Theory Analysis_OCL

(*****************************************************************************
 * Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
 *                       for the OMG Standard.
 *                       http://www.brucker.ch/projects/hol-testgen/
 *
 * Analysis_OCL.thy --- OCL Contracts and an Example.
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2012-2015 Université Paris-Saclay, Univ. Paris-Sud, France
 *               2013-2015 IRT SystemX, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************)

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 
(* To be generated generically ... hard, but crucial lemma that should hold. 
   It means that X and it successor are object representation that actually
   occur in the state. *)

lemma REC_pre : "τ ⊨ Person_label⇩g⇩l⇩o⇩b⇩a⇩l⇩i⇩n⇩v 
       ⟹ τ ⊨ Person .allInstances()->includes⇩S⇩e⇩t(X) ― ‹‹X› represented object in state›
       ⟹ ∃ REC.  τ ⊨ REC(X)  ≜ (Person_label⇩i⇩n⇩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 ...*)       

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 (* Let's hope that this holds ... *)


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 (* Let's hope that this holds ... *)

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) ∧                            ― ‹pre›
            (τ ⊨ (res ≜ if (self).boss@pre ≐ null  ― ‹post›
                         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)  (* an extremely hacky proof that cries for reformulation and automation - bu *)

         
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