Commit 6217cc5b authored by Lawrence Paulson's avatar Lawrence Paulson

new entry, Featherweight_OCL

parent daed7dff550f
This diff is collapsed.
This diff is collapsed.
(*****************************************************************************
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.4
* for the OMG Standard.
* http://www.brucker.ch/projects/hol-testgen/
*
* OCL_main.thy ---
* This file is part of HOL-TestGen.
*
* Copyright (c) 2012-2013 Université Paris-Sud, 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 OCL_main
imports OCL_lib OCL_state OCL_tools
begin
end
This diff is collapsed.
(*****************************************************************************
* Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.4
* for the OMG Standard.
* http://www.brucker.ch/projects/hol-testgen/
*
* OCL_tools.thy ---
* This file is part of HOL-TestGen.
*
* Copyright (c) 2012 Université Paris-Sud, 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 OCL_tools
imports OCL_core
begin
end
chapter AFP
session "Featherweight_OCL (AFP)" = HOL +
description {* Featherweight-OCL *}
options [document = pdf, document_variants="document:outline=/proof,/ML"]
theories
"OCL_main"
"examples/Employee_AnalysisModel_OCLPart"
"examples/Employee_DesignModel_OCLPart"
files
"document/conclusion.tex"
"document/formalization.tex"
"document/hol-ocl-isar.sty"
"document/introduction.tex"
"document/lstisar.sty"
"document/prooftree.sty"
"document/root.bib"
"document/root.tex"
"document/figures/AbstractSimpleChair.pdf"
"document/figures/jedit.png"
"document/figures/pdf.png"
"document/figures/person.png"
"document/figures/pre-post.pdf"
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="brucker@spamfence.net wolff@lri.fr frederic.tuong@lri.fr"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="no"
This diff is collapsed.
input metafun;
boolean cmykcolors;
cmykcolors := false;
input latexmp;
setupLaTeXMP(
% preamblefile="preamble"
class="scrbook"
,options="10pt"
,fontencoding="T1"
,inputencoding="latin1"
,packages=("babel[ngerman,USenglish]"
&",lmodern,hol-ocl-isar")
,preamble=("\renewcommand\familydefault{\ttdefault}")
,mode=normal
% ,multicolor=enable
);
boolean metauml_defaultLaTeX;
metauml_defaultLaTeX := true;
input metauml;
color MaroonFifty;
MaroonFifty := cmyk(0.00, 0.435, 0.34, 0.16);
beginfig(1)
%% Role Hierarchie
AbstractClass.Role("Role")()();
Class.Hearer("Hearer")()();
Class.Speaker("Speaker")()();
Class.Chair("Chair")()();
Class.CoChair("CoCair")()();
topToBottom(30)(Role, Hearer, Speaker);
topToBottom(30)(CoChair, Chair);
leftToRight(25)(Hearer, CoChair);
drawObjects(Role, Hearer, Speaker);
drawObjects(CoChair, Chair);
link(inheritance)(Hearer.n -- Role.s);
link(inheritance)(Speaker.n -- Hearer.s);
link(inheritance)(CoChair.w -- Hearer.e);
link(inheritance)(Chair.n -- CoChair.s);
Class.Person("Person")("+name:String")();
Class.Participant("Participant")()();
Participant.n = Person.e + (Role.w - Person.e)/2 + (0,-30);
leftToRight(100)(Person, Role);
topToBottom(47)(Person, Session);
Class.Session("Session")("+name:String")
(
%"+invite(p:Person):OclVoid",
"+findRole(p:Person):Role");
drawObjects(Person, Session,Participant);
% AssocClass
link(association) (Person.e -- Role.w);
item(iAssoc)("person")(obj.sw = Person.e);
item(iAssoc)("0..*")(obj.nw = Person.e);
%
item(iAssoc)("role")(obj.se = Role.w);
item(iAssoc)("0..*")(obj.ne = Role.w);
item(iAssoc)("0..*")(obj.ne = Participant.w);
link(dashedLink)(Participant.n -- (Person.e+(Role.w-Person.e)/2));
path p;
p = fullcircle scaled 6bp shifted (Person.e+(Role.w-Person.e)/2);
fill p withcolor white;
draw p;
%%%
link(association) (pathManhattanX(Participant.w,(Session.n+(-10,0))));
item(iAssoc)("session")(obj.sw = Session.n+(-10,0));
item(iAssoc)("0..1")(obj.se = Session.n+(-10,0));
endfig;
end
\part{A Proposal for Formal Semantics of OCL 2.5}
% \input{session}
\input{OCL_core.tex}
\input{OCL_lib.tex}
\input{OCL_state.tex}
\input{OCL_tools.tex}
\input{OCL_main.tex}
\renewcommand{\isamarkupheader}[1]{\section{#1}}
\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\paragraph{#1}}
\renewcommand{\isamarkupsect}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsect}[1]{\paragraph{#1}}
\renewcommand{\isamarkupsubsubsect}[1]{\paragraph{#1}}
\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:
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment