.. General-algebraic-execution-rules, 101 Execution Rules on Excluding 102 Execution Rules on Includes 104 Execution Rules on Excludes 105 Execution Rules on Size 105 Execution Rules on 106 Execution Rules on, 101 Execution Rules on Including 107 Execution Rules on Reject . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Execution Rules Combining Previous Operators, p.107

P. B. Andrews, Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2002.
DOI : 10.1007/978-94-015-9934-4

C. Barrett and C. Tinelli, CVC3, Lecture Notes in Computer Science, vol.4590, pp.298-302, 2007.
DOI : 10.1007/978-3-540-73368-3_34

J. C. Blanchette and T. Nipkow, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Lecture Notes in Computer Science, vol.6172, pp.131-146978, 2010.
DOI : 10.1007/978-3-642-14052-5_11

]. A. Brucker, An Interactive Proof Environment for Object-oriented Specifications

A. D. Brucker and B. Wolff, A Proposal for a Formal OCL Semantics in Isabelle/HOL, Theorem Proving in Higher Order Logics (TPHOLs), number 2410 in Lecture Notes in Computer Science, pp.99-114, 2002.
DOI : 10.1007/3-540-45685-6_8

A. D. Brucker, B. Wolff, and E. Zurich, The HOL-OCL book, 2006.

A. D. Brucker and B. Wolff, An Extensible Encoding of Object-oriented Data Models in hol, Journal of Automated Reasoning, vol.10, issue.2, pp.219-249, 2008.
DOI : 10.1007/s10817-008-9108-3
URL : https://hal.archives-ouvertes.fr/hal-01214567

A. D. Brucker and B. Wolff, Semantics, calculi, and analysis for object-oriented specifications, Acta Informatica, vol.39, issue.2, pp.255-284, 2009.
DOI : 10.1007/s00236-009-0093-8
URL : https://hal.archives-ouvertes.fr/hal-01214519

A. D. Brucker, J. Doser, and B. Wolff, Semantic issues of OCL: Past, present, and future, Electronic Communications of the EASST, vol.5, 2006.

A. D. Brucker, J. Doser, and B. Wolff, A model transformation semantics and analysis methodology for SecureUML Model Driven Engineering Languages and Systems, number 4199 in Lecture Notes in Computer Science, MoDELS, pp.306-320, 2006.

A. D. Brucker, M. P. Krieger, and B. Wolff, Extending OCL with null-references Models in Software Engineering, number 6002 in Lecture Notes in Computer Science, pp.261-275, 2009.

A. D. Brucker, M. P. Krieger, D. Longuet, B. Wolff, and U. Ocl, A specification-based test case generation method for MoDELS Workshops, number 6627 in Lecture Notes in Computer Science, pp.334-348, 2010.

A. D. Brucker, D. Chiorean, T. Clark, B. Demuth, M. Gogolla et al., Report on the Aachen OCL meeting, Proceedings of the MODELS 2013 OCL Workshop (OCL 2013), volume 1092 of CEUR Workshop Proceedings

A. D. Brucker, D. Longuet, F. Tuong, and B. Wolff, On the semantics of object-oriented data structures and path expressions, Proceedings of the models 2013 ocl Workshop volume 1092 of ceur Workshop Proceedings, pp.23-32, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01214460

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

T. Clark and J. Warmer, Object Modeling with the OCL: The Rationale behind the Object Constraint Language, Lecture Notes in Computer Science, vol.2263, 2002.
DOI : 10.1007/3-540-45669-4

S. Cook, A. Kleppe, R. Mitchell, B. Rumpe, J. Warmer et al., The Amsterdam Manifesto on OCL, pp.115-149
DOI : 10.1007/3-540-45669-4_7

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Lecture Notes in Computer Science, vol.4963, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

M. Gogolla and M. Richters, Expressing UML Class Diagrams Properties with OCL, pp.85-114
DOI : 10.1007/3-540-45669-4_6

F. Haftmann and M. Wenzel, Constructive Type Classes in Isabelle, Types for Proofs and Programs, International Workshop, pp.160-174, 2006.
DOI : 10.1007/978-3-540-74464-1_11

A. Hamie, F. Civello, J. Howse, S. Kent, and R. Mitchell, Reflections on the Object Constraint Language, The Unified Modeling Language. «UML»'98: Beyond the Notation, pp.162-172, 1998.
DOI : 10.1007/978-3-540-48480-6_13

P. Kosiuczenko, Specification of Invariability in OCL, Model Driven Engineering Languages and Systems (MoDELS), pp.676-691, 2006.
DOI : 10.1007/11880240_47

M. P. Krieger, A. Knapp, and B. Wolff, Generative programming and component engineering, International Conference on Generative Programming and Component Engineering, pp.53-62, 2010.

G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby et al., jml reference manual (revision 1.2), Feb Available from http, 2007.

L. Mandel and M. V. Cengarle, On the Expressive Power of OCL, World Congress on Formal Methods in the Development of Computing Systems (FM), pp.854-874, 1999.
DOI : 10.1007/3-540-48119-2_47

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL?A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, pp.10-1007, 2002.

M. Object and . Group, Object constraint language specification (version 1.1), Sept Available as OMG document ad, pp.97-105, 1997.

M. Object and . Group, UML 2.4.1: Superstructure specification Available as OMG document formal, pp.2011-2019, 2011.

M. Object and . Group, UML 2.3.1 OCL specification, Feb. 2012. Available as OMG document formal, pp.2012-2013

M. Richters, A Precise Approach to Validating UML Models and OCL Constraints, 2002.

E. Torlak and D. Jackson, Kodkod: A Relational Model Finder, Lecture Notes in Computer Science, vol.4424, pp.632-647, 2007.
DOI : 10.1007/978-3-540-71209-1_49

M. Wenzel and B. Wolff, Building Formal Method Tools in the Isabelle/Isar Framework, TPHOLs 2007, number 4732 in Lecture Notes in Computer Science, pp.352-367978, 2007.
DOI : 10.1007/978-3-540-74591-4_26

M. M. Wenzel and T. München, Isabelle/Isar ? a versatile environment for human-readable formal proof documents, 2002.