git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13174 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Frédéric Tuong 2017-10-14 04:22:00 +00:00
parent d0ec336493
commit 5f8bdb26a1
2 changed files with 48 additions and 0 deletions

48
README.md Normal file
View File

@ -0,0 +1,48 @@
# HOL-OCL 2.0
HOL-OCL 2.0 is a successor of
[HOL-OCL](https://www.brucker.ch/projects/hol-ocl/), an interactive
proof environment for the *Object Constraint Language (OCL)*. HOL-OCL
2.0 as a tool is based on a library defining its core semantic
concepts called [Featherweight
OCL](https://www.isa-afp.org/entries/Featherweight_OCL.shtml), which
also serves as basis for the ongoing OCL 2.5 standardisation at the
OMG.
HOL-OCL 2.0 addresses the fragment in UML concerned with
object-oriented data modelling. Thus, it comes with a number of
packages related with the semantic constructions and instantiations of
objects, among other the *Class Model Package* to set up the
underlying object-oriented datatype theory, or the *Invariant &
Operation Package* supporting a formal contract language to define
methods issued from a class model.
## Authors
* [Achim D. Brucker](http://www.brucker.ch/)
* Frédéric Tuong
* [Burkhart Wolff](https://www.lri.fr/~wolff/)
## License
This project is licensed under a 3-clause BSD-style license.
## Publications
* Frédéric Tuong. Constructing Semantically Sound Object-Logics for
UML/OCL Based Domain-Specific Languages. Université Paris-Sud, IRT
SystemX, LRI, CNRS, CentraleSupélec, Université Paris-Saclay, 2016.
https://tel.archives-ouvertes.fr/tel-01318156, Formal proof
development.
* Frédéric Tuong, and Burkhart Wolff. A Meta-Model for the Isabelle API. In
Archive of Formal Proofs, 2015.
http://www.isa-afp.org/entries/Isabelle_Meta_Model.shtml, Formal proof
development.
* Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight
OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. In
Archive of Formal Proofs, 2014.
http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal proof
development.
* Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for
the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and
Textual Modelling (OCL 2012), pages 19-24, 2012.
https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012