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_labelinv :: "Person  Boolean" 
where     "Person_labelinv (self)   
                 (self .boss <> null implies (self .salary  int  ((self .boss) .salary)))"
                                       

definition Person_labelinvATpre :: "Person  Boolean" 
where     "Person_labelinvATpre (self)   
                 (self .boss@pre <> null implies (self .salary@pre int ((self .boss@pre) .salary@pre)))"

definition Person_labelglobalinv :: "Boolean"
where     "Person_labelglobalinv  (Person .allInstances()->forAllSet(x | Person_labelinv (x)) and 
                                  (Person .allInstances@pre()->forAllSet(x | Person_labelinvATpre (x))))"
                                  
                                  
lemma "τ  δ (X .boss)  τ  Person .allInstances()->includesSet(X .boss) 
                            τ  Person .allInstances()->includesSet(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_labelglobalinv 
        τ  Person .allInstances()->includesSet(X) ― ‹X› represented object in state›
         REC.  τ  REC(X)   (Person_labelinv (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 invPerson_label :: "Person  Boolean"
where invPerson_label_def:
"(τ  Person .allInstances()->includesSet(self))  
 (τ  (invPerson_label(self)   (self .boss <> null implies  
                                  (self .salary  int  ((self .boss) .salary)) and
                                   invPerson_label(self .boss))))"

axiomatization invPerson_labelATpre :: "Person  Boolean"
where invPerson_labelATpre_def: 
"(τ  Person .allInstances@pre()->includesSet(self)) 
 (τ  (invPerson_labelATpre(self)  (self .boss@pre <> null implies 
                                   (self .salary@pre  int  ((self .boss@pre) .salary@pre)) and
                                    invPerson_labelATpre(self .boss@pre))))"


lemma inv_1 : 
"(τ  Person .allInstances()->includesSet(self)) 
    (τ  invPerson_label(self) = ((τ  (self .boss  null)) 
                               ( τ  (self .boss <> null)  
                                 τ  ((self .salary)  int  (self .boss .salary))  
                                 τ  (invPerson_label(self .boss))))) "
oops (* Let's hope that this holds ... *)


lemma inv_2 : 
"(τ  Person .allInstances@pre()->includesSet(self)) 
    (τ  invPerson_labelATpre(self)) =  ((τ  (self .boss@pre  null)) 
                                     (τ  (self .boss@pre <> null) 
                                     (τ  (self .boss@pre .salary@pre int self .salary@pre))  
                                     (τ  (invPerson_labelATpre(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 int 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()
                                                       ->includingSet(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()
                                                       ->includingSet(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()
                                                       ->includingSet(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) StrictRefEqObject_Person cp_StrictRefEqObject cp_dotPersonℬ𝒪𝒮𝒮)
            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_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴) by simp
            have C:"self τ. ((λ_. self τ).boss .contents()->includingSet((λ_. self τ).salary) τ) = 
                              (self .boss .contents() ->includingSet(self .salary) τ)" 
                   apply(subst UML_Set.OclIncluding.cp0) apply(subst (2) UML_Set.OclIncluding.cp0)   
                   apply(subst (2) Analysis_UML.cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴)
                   apply(subst cp0_contents)  apply(subst (2) cp0_contents)
                   apply(subst (2) cp_dotPersonℬ𝒪𝒮𝒮) by simp
            show "self res τ.
                   (res  if (self .boss)  null then Set{self .salary} 
                           else self .boss .contents()->includingSet(self .salary) endif) τ =
                   ((λ_. res τ)  if (λ_. self τ) .boss  null then Set{(λ_. self τ) .salary} 
                                   else(λ_. self τ) .boss .contents()->includingSet((λ_. 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()->includingSet(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()
                                    ->includingSet(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()
                                                                        ->includingSet(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()->includingSet(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 StrictRefEqObject_Person cp_StrictRefEqObject cp_dotPersonℬ𝒪𝒮𝒮_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_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre) by simp
            have C:"self τ. ((λ_. self τ).boss@pre .contents@pre()->includingSet((λ_. self τ).salary@pre) τ) = 
                              (self .boss@pre .contents@pre() ->includingSet(self .salary@pre) τ)" 
                   apply(subst UML_Set.OclIncluding.cp0) apply(subst (2) UML_Set.OclIncluding.cp0)   
                   apply(subst (2) Analysis_UML.cp_dotPerson𝒮𝒜ℒ𝒜ℛ𝒴_at_pre)
                   apply(subst cp0_contents_at_pre)  apply(subst (2) cp0_contents_at_pre)
                   apply(subst (2) cp_dotPersonℬ𝒪𝒮𝒮_at_pre) by simp
           show "self res τ.
                   (res  if (self .boss@pre)  null then Set{self .salary@pre} 
                           else self .boss@pre .contents@pre()->includingSet(self .salary@pre) endif) τ =
                   ((λ_. res τ)  if (λ_. self τ) .boss@pre  null then Set{(λ_. self τ) .salary@pre} 
                                   else(λ_. self τ) .boss@pre .contents@pre()->includingSet((λ_. 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()->includingSet(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()->includingSet(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()->includingSet(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.cpPRE}  & @{thm  [display=false] insert.cpPRE} \\
      @{thm [source] insert.cpPOST}  & @{thm  [display=false] insert.cpPOST} \\
      @{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