Commit e68e1996 authored by Frédéric Tuong's avatar Frédéric Tuong

synchronize with hol-testgen/r12148

parent 57bb43378d6f
(*****************************************************************************
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
* for the OMG Standard.
* http://www.brucker.ch/projects/hol-testgen/
*
* This file is part of HOL-TestGen.
*
* Copyright (c) 2013-2015 Université Paris-Saclay, Univ. Paris-Sud, France
* 2013-2015 IRT SystemX, France
* 2013-2015 Achim D. Brucker, Germany
*
* 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.
******************************************************************************)
chapter AFP
session Featherweight_OCL (AFP) = HOL +
session Featherweight_OCL (AFP) in "src" = HOL +
description {* Featherweight-OCL *}
options [document_variants = "document:outline=/proof,/ML"]
options [document_variants = "annex-a=annexa,-theory,-afp,-proof,-ML:document=afp,-annexa:outline=-annexa,afp,/proof,/ML",
show_question_marks = false]
theories
"OCL_main"
"examples/Employee_AnalysisModel_OCLPart"
"examples/Employee_DesignModel_OCLPart"
"UML_Main"
"../examples/Employee_Model/Analysis/Analysis_OCL"
"../examples/Employee_Model/Design/Design_OCL"
document_files
"conclusion.tex"
"formalization.tex"
"figures/AbstractSimpleChair.pdf"
"figures/jedit.png"
"figures/pdf.png"
"figures/person.png"
"figures/pre-post.pdf"
"hol-ocl-isar.sty"
"introduction.tex"
"lstisar.sty"
"omg.sty"
"prooftree.sty"
"root.bib"
"root.tex"
"figures/AbstractSimpleChair.pdf"
"figures/jedit.png"
"figures/pdf.png"
"figures/person.png"
"figures/pre-post.pdf"
"FOCL_Syntax.tex"
\part{A Proposal for Formal Semantics of OCL 2.5}
\input{OCL_core.tex}
\input{OCL_lib.tex}
\input{OCL_state.tex}
\input{OCL_tools.tex}
\input{OCL_main.tex}
\part{Examples}
\chapter{The Employee Analysis Model}
\label{ex:employee-analysis}
\input{Employee_AnalysisModel_UMLPart.tex}
\input{Employee_AnalysisModel_OCLPart.tex}
\chapter{The Employee Design Model}
\label{ex:employee-design}
\input{Employee_DesignModel_UMLPart.tex}
\input{Employee_DesignModel_OCLPart.tex}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:
\documentclass[fontsize=11pt,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage{fixltx2e}
\usepackage{isabelle,isabellesym}
\usepackage[nocolortable, noaclist]{hol-ocl-isar}
\usepackage{booktabs}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage[caption=false]{subfig}
\usepackage{lstisar}
\usepackage{tabu}
\usepackage[]{mathtools}
\usepackage{prooftree}
\usepackage[english]{babel}
\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
% \usepackage[draft]{fixme}
% MathOCl expressions
\colorlet{MathOclColor}{Black}
\colorlet{HolOclColor}{Black}
\colorlet{OclColor}{Black}
%
\sloppy
\uchyph=0
\graphicspath{{data/},{figures/}}
\allowdisplaybreaks
\renewcommand{\HolTrue}{\mathrm{true}}
\renewcommand{\HolFalse}{\mathrm{false}}
\newcommand{\ptmi}[1]{\using{\mi{#1}}}
\newcommand{\Lemma}[1]{{\color{BrickRed}%
\mathbf{\operatorname{lemma}}}~\text{#1:}\quad}
\newcommand{\done}{{\color{OliveGreen}\operatorname{done}}}
\newcommand{\apply}[1]{{\holoclthykeywordstyle%
\operatorname{apply}}(\text{#1})}
\newcommand{\fun} {{\holoclthykeywordstyle\operatorname{fun}}}
\newcommand{\definitionS} {{\holoclthykeywordstyle\operatorname{definition}}}
\newcommand{\where} {{\holoclthykeywordstyle\operatorname{where}}}
\newcommand{\datatype} {{\holoclthykeywordstyle\operatorname{datatype}}}
\newcommand{\types} {{\holoclthykeywordstyle\operatorname{types}}}
\newcommand{\pglabel}[1]{\text{#1}}
\renewcommand{\isasymOclUndefined}{\ensuremath{\mathtt{invalid}}}
\newcommand{\isasymOclNull}{\ensuremath{\mathtt{null}}}
\newcommand{\isasymOclInvalid}{\isasymOclUndefined}
\DeclareMathOperator{\inv}{inv}
\newcommand{\Null}[1]{{\ensuremath{\mathtt{null}_\text{{#1}}}}}
\newcommand{\testgen}{HOL-TestGen\xspace}
\newcommand{\HolOption}{\mathrm{option}}
\newcommand{\ran}{\mathrm{ran}}
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\typedef}{\mathrm{typedef}}
\newcommand{\mi}[1]{\,\text{#1}}
\newcommand{\state}[1]{\ifthenelse{\equal{}{#1}}%
{\operatorname{state}}%
{\operatorname{\mathit{state}}(#1)}%
}
\newcommand{\mocl}[1]{\text{\inlineocl|#1|}}
\DeclareMathOperator{\TCnull}{null}
\DeclareMathOperator{\HolNull}{null}
\DeclareMathOperator{\HolBot}{bot}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\begin{document}
\renewcommand{\subsubsectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\chapterautorefname}{Chapter}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\title{Featherweight OCL}
\subtitle{A Proposal for a Machine-Checked Formal Semantics for OCL 2.5}
\author{%
\href{http://www.brucker.ch/}{Achim D. Brucker}\footnotemark[1]
\and
\href{https://www.lri.fr/~tuong/}{Fr\'ed\'eric Tuong}\footnotemark[3]
\and
\href{https://www.lri.fr/~wolff/}{Burkhart Wolff}\footnotemark[2]}
\publishers{%
\footnotemark[1]~SAP AG, Vincenz-Priessnitz-Str. 1, 76131 Karlsruhe,
Germany \texorpdfstring{\\}{} \href{mailto:"Achim D. Brucker"
<achim.brucker@sap.com>}{achim.brucker@sap.com}\\[2em]
%
\footnotemark[3]~Univ. Paris-Sud, IRT SystemX, 8 av.~de la Vauve, \\
91120 Palaiseau, France\\
frederic.tuong@\{u-psud, irt-systemx\}.fr\\[2em]
%
\footnotemark[2]~Univ. Paris-Sud, Laboratoire LRI, UMR8623, 91405 Orsay, France\\
CNRS, 91405 Orsay, France\texorpdfstring{\\}{}
\href{mailto:"Burkhart Wolff" <burkhart.wolff@lri.fr>}{burkhart.wolff@lri.fr}
}
\maketitle
\begin{abstract}
The Unified Modeling Language (UML) is one of the few modeling
languages that is widely used in industry. While UML is mostly known
as diagrammatic modeling language (\eg, visualizing class models),
it is complemented by a textual language, called Object Constraint
Language (OCL). OCL is a textual annotation language, based on a
three-valued logic, that turns UML into a formal language.
Unfortunately the semantics of this specification language, captured
in the ``Annex A'' of the OCL standard, leads to different
interpretations of corner cases. Many of these corner cases had
been subject to formal analysis since more than ten years.
The situation complicated when with version 2.3 the OCL was aligned
with the latest version of UML: this led to the extension of the
three-valued logic by a second exception element, called
\inlineocl{null}. While the first exception element
\inlineocl{invalid} has a strict semantics, \inlineocl{null} has a
non strict semantic interpretation. These semantic difficulties lead
to remarkable confusion for implementors of OCL compilers and
interpreters.
In this paper, we provide a formalization of the core of OCL in
HOL\@. It provides denotational definitions, a logical calculus and
operational rules that allow for the execution of OCL expressions by
a mixture of term rewriting and code compilation. Our formalization
reveals several inconsistencies and contradictions in the current
version of the OCL standard. They reflect a challenge to define and
implement OCL tools in a uniform manner. Overall, this document is
intended to provide the basis for a machine-checked text ``Annex A''
of the OCL standard targeting at tool implementors.
\end{abstract}
\tableofcontents
\include{introduction}
\include{formalization}
\include{conclusion}
\bibliographystyle{abbrvnat}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
% LocalWords: implementors denotational OCL UML
(*****************************************************************************
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.4
* for the OMG Standard.
* http://www.brucker.ch/projects/hol-testgen/
*
* Employee_DesignModel_OCLPart.thy --- OCL Contracts and an Example.
* This file is part of HOL-TestGen.
*
* Copyright (c) 2012-2013 Université Paris-Sud, France
* 2013 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.
******************************************************************************)
section{* The Employee Analysis Model (OCL) *}
theory
Employee_AnalysisModel_OCLPart
imports
Employee_AnalysisModel_UMLPart
begin
text {* \label{ex:employee-analysis:ocl} *}
subsection{* Standard State Infrastructure *}
text{* Ideally, these definitions are automatically generated from the class model. *}
subsection{* Invariant *}
text{* These recursive predicates can be defined conservatively
by greatest fix-point
constructions---automatically. See~\cite{brucker.ea:hol-ocl-book:2006,brucker:interactive:2007}
for details. For the purpose of this example, we state them as axioms
here. *}
axiomatization inv_Person :: "Person \<Rightarrow> Boolean"
where A : "(\<tau> \<Turnstile> (\<delta> self)) \<longrightarrow>
(\<tau> \<Turnstile> inv_Person(self)) =
((\<tau> \<Turnstile> (self .boss \<doteq> null)) \<or>
( \<tau> \<Turnstile> (self .boss <> null) \<and> (\<tau> \<Turnstile> ((self .salary) `\<le> (self .boss .salary))) \<and>
(\<tau> \<Turnstile> (inv_Person(self .boss))))) "
axiomatization inv_Person_at_pre :: "Person \<Rightarrow> Boolean"
where B : "(\<tau> \<Turnstile> (\<delta> self)) \<longrightarrow>
(\<tau> \<Turnstile> inv_Person_at_pre(self)) =
((\<tau> \<Turnstile> (self .boss@pre \<doteq> null)) \<or>
( \<tau> \<Turnstile> (self .boss@pre <> null) \<and>
(\<tau> \<Turnstile> (self .boss@pre .salary@pre `\<le> self .salary@pre)) \<and>
(\<tau> \<Turnstile> (inv_Person_at_pre(self .boss@pre))))) "
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 \<Rightarrow> (\<AA>)st \<Rightarrow> bool" where
"(\<tau> \<Turnstile> (\<delta> self)) \<Longrightarrow> ((\<tau> \<Turnstile> (self .boss \<doteq> null)) \<or>
(\<tau> \<Turnstile> (self .boss <> null) \<and> (\<tau> \<Turnstile> (self .boss .salary `\<le> self .salary)) \<and>
( (inv(self .boss))\<tau> )))
\<Longrightarrow> ( inv self \<tau>)"
subsection{* The Contract of a Recursive Query *}
text{* The original specification of a recursive query :
\begin{ocl}
context Person::contents():Set(Integer)
post: result = if self.boss = null
then Set{i}
else self.boss.contents()->including(i)
endif
\end{ocl} *}
consts dot_contents :: "Person \<Rightarrow> Set_Integer" ("(1(_).contents'('))" 50)
axiomatization where dot_contents_def:
"(\<tau> \<Turnstile> ((self).contents() \<triangleq> result)) =
(if (\<delta> self) \<tau> = true \<tau>
then ((\<tau> \<Turnstile> true) \<and>
(\<tau> \<Turnstile> (result \<triangleq> if (self .boss \<doteq> null)
then (Set{self .salary})
else (self .boss .contents()->including(self .salary))
endif)))
else \<tau> \<Turnstile> result \<triangleq> invalid)"
consts dot_contents_AT_pre :: "Person \<Rightarrow> Set_Integer" ("(1(_).contents@pre'('))" 50)
axiomatization where dot_contents_AT_pre_def:
"(\<tau> \<Turnstile> (self).contents@pre() \<triangleq> result) =
(if (\<delta> self) \<tau> = true \<tau>
then \<tau> \<Turnstile> true \<and> (* pre *)
\<tau> \<Turnstile> (result \<triangleq> if (self).boss@pre \<doteq> null (* post *)
then Set{(self).salary@pre}
else (self).boss@pre .contents@pre()->including(self .salary@pre)
endif)
else \<tau> \<Turnstile> result \<triangleq> invalid)"
text{* These \inlineocl{@pre} variants on methods are only available on queries, \ie,
operations without side-effect. *}
subsection{* The Contract of a Method *}
text{*
The specification in high-level OCL input syntax reads as follows:
\begin{ocl}
context Person::insert(x:Integer)
post: contents():Set(Integer)
contents() = contents@pre()->including(x)
\end{ocl}
*}
consts dot_insert :: "Person \<Rightarrow> Integer \<Rightarrow> Void" ("(1(_).insert'(_'))" 50)
axiomatization where dot_insert_def:
"(\<tau> \<Turnstile> ((self).insert(x) \<triangleq> result)) =
(if (\<delta> self) \<tau> = true \<tau> \<and> (\<upsilon> x) \<tau> = true \<tau>
then \<tau> \<Turnstile> true \<and>
\<tau> \<Turnstile> ((self).contents() \<triangleq> (self).contents@pre()->including(x))
else \<tau> \<Turnstile> ((self).insert(x) \<triangleq> invalid))"
end
(*****************************************************************************
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.4
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
* for the OMG Standard.
* http://www.brucker.ch/projects/hol-testgen/
*
* Employee_DesignModel_OCLPart.thy --- OCL Contracts and an Example.
* Design_OCL.thy --- OCL Contracts and an Example.
* This file is part of HOL-TestGen.
*
* Copyright (c) 2012-2013 Université Paris-Sud, France
* 2013 IRT SystemX, France
* Copyright (c) 2012-2015 Université Paris-Saclay, Univ. Paris-Sud, France
* 2013-2015 IRT SystemX, France
*
* All rights reserved.
*
......@@ -40,104 +40,98 @@
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
section{* The Employee Design Model (OCL) *}
theory
Employee_DesignModel_OCLPart
Design_OCL
imports
Employee_DesignModel_UMLPart
Design_UML
begin
text {* \label{ex:employee-design:ocl} *}
subsection{* Standard State Infrastructure *}
text{* Ideally, these definitions are automatically generated from the class model. *}
subsection{* Invariant *}
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,brucker:interactive:2007}
for details. For the purpose of this example, we state them as axioms
here. *}
axiomatization inv_Person :: "Person \<Rightarrow> Boolean"
where A : "(\<tau> \<Turnstile> (\<delta> self)) \<longrightarrow>
(\<tau> \<Turnstile> inv_Person(self)) =
((\<tau> \<Turnstile> (self .boss \<doteq> null)) \<or>
( \<tau> \<Turnstile> (self .boss <> null) \<and> (\<tau> \<Turnstile> ((self .salary) `\<le> (self .boss .salary))) \<and>
(\<tau> \<Turnstile> (inv_Person(self .boss))))) "
axiomatization inv_Person_at_pre :: "Person \<Rightarrow> Boolean"
where B : "(\<tau> \<Turnstile> (\<delta> self)) \<longrightarrow>
(\<tau> \<Turnstile> inv_Person_at_pre(self)) =
((\<tau> \<Turnstile> (self .boss@pre \<doteq> null)) \<or>
( \<tau> \<Turnstile> (self .boss@pre <> null) \<and>
(\<tau> \<Turnstile> (self .boss@pre .salary@pre `\<le> self .salary@pre)) \<and>
(\<tau> \<Turnstile> (inv_Person_at_pre(self .boss@pre))))) "
here.
\begin{ocl}
context Person
inv label : self .boss <> null implies (self .salary \<le> ((self .boss) .salary))
\end{ocl}
*}
definition Person_label\<^sub>i\<^sub>n\<^sub>v :: "Person \<Rightarrow> Boolean"
where "Person_label\<^sub>i\<^sub>n\<^sub>v (self) \<equiv>
(self .boss <> null implies (self .salary \<le>\<^sub>i\<^sub>n\<^sub>t ((self .boss) .salary)))"
definition Person_label\<^sub>i\<^sub>n\<^sub>v\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e :: "Person \<Rightarrow> Boolean"
where "Person_label\<^sub>i\<^sub>n\<^sub>v\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e (self) \<equiv>
(self .boss@pre <> null implies (self .salary@pre \<le>\<^sub>i\<^sub>n\<^sub>t ((self .boss@pre) .salary@pre)))"
definition Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>i\<^sub>n\<^sub>v :: "Boolean"
where "Person_label\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>i\<^sub>n\<^sub>v \<equiv> (Person .allInstances()->forAll\<^sub>S\<^sub>e\<^sub>t(x | Person_label\<^sub>i\<^sub>n\<^sub>v (x)) and
(Person .allInstances@pre()->forAll\<^sub>S\<^sub>e\<^sub>t(x | Person_label\<^sub>i\<^sub>n\<^sub>v\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e (x))))"
lemma "\<tau> \<Turnstile> \<delta> (X .boss) \<Longrightarrow> \<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(X .boss) \<and>
\<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>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 : "\<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> \<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 ...*)
text{* This allows to state a predicate: *}
axiomatization inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l :: "Person \<Rightarrow> Boolean"
where inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l_def:
"(\<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(self)) \<Longrightarrow>
(\<tau> \<Turnstile> (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l(self) \<triangleq> (self .boss <> null implies
(self .salary \<le>\<^sub>i\<^sub>n\<^sub>t ((self .boss) .salary)) and
inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l(self .boss))))"
axiomatization inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e :: "Person \<Rightarrow> Boolean"
where inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e_def:
"(\<tau> \<Turnstile> Person .allInstances@pre()->includes\<^sub>S\<^sub>e\<^sub>t(self)) \<Longrightarrow>
(\<tau> \<Turnstile> (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e(self) \<triangleq> (self .boss@pre <> null implies
(self .salary@pre \<le>\<^sub>i\<^sub>n\<^sub>t ((self .boss@pre) .salary@pre)) and
inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e(self .boss@pre))))"
lemma inv_1 :
"(\<tau> \<Turnstile> Person .allInstances()->includes\<^sub>S\<^sub>e\<^sub>t(self)) \<Longrightarrow>
(\<tau> \<Turnstile> inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l(self) = ((\<tau> \<Turnstile> (self .boss \<doteq> null)) \<or>
( \<tau> \<Turnstile> (self .boss <> null) \<and>
\<tau> \<Turnstile> ((self .salary) \<le>\<^sub>i\<^sub>n\<^sub>t (self .boss .salary)) \<and>
\<tau> \<Turnstile> (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l(self .boss))))) "
oops (* Let's hope that this holds ... *)
lemma inv_2 :
"(\<tau> \<Turnstile> Person .allInstances@pre()->includes\<^sub>S\<^sub>e\<^sub>t(self)) \<Longrightarrow>
(\<tau> \<Turnstile> inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>e(self)) = ((\<tau> \<Turnstile> (self .boss@pre \<doteq> null)) \<or>
(\<tau> \<Turnstile> (self .boss@pre <> null) \<and>
(\<tau> \<Turnstile> (self .boss@pre .salary@pre \<le>\<^sub>i\<^sub>n\<^sub>t self .salary@pre)) \<and>
(\<tau> \<Turnstile> (inv\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n\<^sub>_\<^sub>l\<^sub>a\<^sub>b\<^sub>e\<^sub>l\<^sub>A\<^sub>T\<^sub>p\<^sub>r\<^sub>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 \<Rightarrow> (\<AA>)st \<Rightarrow> bool" where
"(\<tau> \<Turnstile> (\<delta> self)) \<Longrightarrow> ((\<tau> \<Turnstile> (self .boss \<doteq> null)) \<or>
(\<tau> \<Turnstile> (self .boss <> null) \<and> (\<tau> \<Turnstile> (self .boss .salary `\<le> self .salary)) \<and>
(\<tau> \<Turnstile> (self .boss <> null) \<and> (\<tau> \<Turnstile> (self .boss .salary \<le>\<^sub>i\<^sub>n\<^sub>t self .salary)) \<and>
( (inv(self .boss))\<tau> )))
\<Longrightarrow> ( inv self \<tau>)"
subsection{* The Contract of a Recursive Query *}
text{* The original specification of a recursive query :
\begin{ocl}
context Person::contents():Set(Integer)
post: result = if self.boss = null
then Set{i}
else self.boss.contents()->including(i)
endif
\end{ocl} *}
consts dot_contents :: "Person \<Rightarrow> Set_Integer" ("(1(_).contents'('))" 50)
axiomatization where dot_contents_def:
"(\<tau> \<Turnstile> ((self).contents() \<triangleq> result)) =
(if (\<delta> self) \<tau> = true \<tau>
then ((\<tau> \<Turnstile> true) \<and>
(\<tau> \<Turnstile> (result \<triangleq> if (self .boss \<doteq> null)
then (Set{self .salary})
else (self .boss .contents()->including(self .salary))
endif)))
else \<tau> \<Turnstile> result \<triangleq> invalid)"
consts dot_contents_AT_pre :: "Person \<Rightarrow> Set_Integer" ("(1(_).contents@pre'('))" 50)
axiomatization where dot_contents_AT_pre_def:
"(\<tau> \<Turnstile> (self).contents@pre() \<triangleq> result) =
(if (\<delta> self) \<tau> = true \<tau>
then \<tau> \<Turnstile> true \<and> (* pre *)
\<tau> \<Turnstile> (result \<triangleq> if (self).boss@pre \<doteq> null (* post *)
then Set{(self).salary@pre}
else (self).boss@pre .contents@pre()->including(self .salary@pre)
endif)
else \<tau> \<Turnstile> result \<triangleq> invalid)"
text{* These \inlineocl{@pre} variants on methods are only available on queries, \ie,
operations without side-effect. *}
subsection{* The Contract of a Method *}
text{*
The specification in high-level OCL input syntax reads as follows:
\begin{ocl}
context Person::insert(x:Integer)
post: contents():Set(Integer)
contents() = contents@pre()->including(x)
\end{ocl}
*}
consts dot_insert :: "Person \<Rightarrow> Integer \<Rightarrow> Void" ("(1(_).insert'(_'))" 50)
section{* OCL Part: The Contract of a Recursive Query *}
text{* This part is analogous to the Analysis Model and skipped here. *}
axiomatization where dot_insert_def:
"(\<tau> \<Turnstile> ((self).insert(x) \<triangleq> result)) =
(if (\<delta> self) \<tau> = true \<tau> \<and> (\<upsilon> x) \<tau> = true \<tau>
then \<tau> \<Turnstile> true \<and>