Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP). https://www.isa-afp.org/entries/Featherweight_OCL.shtml
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
Achim D. Brucker 603afc9bc7 Migration to Isabelle 2020. 8 months ago
..
basic_types Import of official AFP entry for Isabelle 2019. 1 year ago
collection_types Import of official AFP entry for Isabelle 2019. 1 year ago
document Import of official AFP entry for Isabelle 2019. 1 year ago
examples/Employee_Model Import of official AFP entry for Isabelle 2019. 1 year ago
ROOT Migration to Isabelle 2020. 8 months ago
UML_Contracts.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_Library.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_Logic.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_Main.thy Clarified file structure. Official AFP entry is now in directory Featherweight_OCL. 4 years ago
UML_PropertyProfiles.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_State.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_Tools.thy Import of official AFP entry for Isabelle 2019. 1 year ago
UML_Types.thy Import of official AFP entry for Isabelle 2019. 1 year ago
readme.txt Import of current (Isabelle 2017) release of Featherweight OCL. 3 years ago

readme.txt

This directory contains the detailed AFP submission of the
"Featherweight OCL" semantics for OCL as well as our proposal
for Appendix A of the OCL standard.

Beyond the standard mechanism

(* < *)
<<skipped isar text, not shown in doc >>
(* > *)

The two main targets of this Isabelle project are:
- check everything and generate all documents allowing "sorry"'s, i.e.,
using Isabelles "quick-and-dirty"-mode:

isabelle build -c -d . -v -b OCL-dirty

- check everything and generate all documents, ensuring that
no "sorry"'s are used:

isabelle build -c -d . -v -b OCL

In your LaTeX text, you can use the following two PlainTeX
environments for selecting in which version your text should
appear:

\isatagafp
This text will only be visible in the AFP submission, i.e.,
document.pdf and outline.pdf.
\endisatagafp

\isatagannexa
This text will only be visible in the Annex A, i.e., annex-a.pdf.
\endisatagannexa


Note that these tags only work within regular Isabelle/Isar "text"
commands if they are complete, i.e.:

text {* ... \isatagafp ... \endisatagafp ...*}

Only opening or closing such a tag in Isabelle/Isar "text" commands
will not work. For this, you need to use the "text_raw" command:

text_raw {* \isatagafp *}
...
text_raw {* \endisatagafp *}


For working, these tags rely on the file comment.sty, which
is automatically added by Isabelle during the document generation.
However at the time of writing, the current comment.sty included by
Isabelle (version 3.6) mentions:
"The opening and closing commands should appear on a line
of their own. No starting spaces, nothing after it."
In particular, it is not advised to put these tags in a single line:
\isatagafp ... \endisatagafp % wrong
otherwise as side effects some parts occurring after these tags may be
skipped. The recommanded solution is to always write each tag in a
separate line:
\isatagafp
...
\endisatagafp


Warning:
=======
Please check twice that you are using \isatagX and \endisatagX
properly, i.e.,
- always pairwise matching
- not separating other envirments.
Not using these PlainTeX environments (which are, generally,
obsolete and discouraged but used by the Isabelle LaTeX setup
anyhow. We only use them to avoid introducing a parallel setup to
the one that we cannot avoid due to design decisions by the
Isabelle maintainer) carefully, will result in LaTeX errors that
are close to not debug-able.