The HOL-OCL book
Achim D. Brucker, Burkhart Wolff · Repository for Publications and Research Data (ETH Zurich) · 2006
This manual describes HOL-OCL 0.9.0 with referential universes and smashed collection types.The manual of version 0.9.0 is also available as technical report number 525 from the department of computer science, ETH Zurich. context A : inv : self .s -> includes (5)Keywords are printed in a blue typeface.• OCL formulae that are interpreted within HOL-OCL, i. e., are written inline as self .s->includes(5),or alternatively in mathematical syntax as: 5 ∈ (self .s).As you can see, we use a (shorter) mathematical notation for OCL expressions.This notation is introduced as an alternative concrete syntax (see Table A.2 for a syntax comparison).Overall, HOL-OCL supports both notations, but we prefer the mathematical one for semantic definitions and proof work.14 1.4.Acknowledgements• We use a color coding to distinguish OCL and HOL sub-expressions in formulae containing both, e. g.:Overall, HOL expressions are printed using the default color.We resolve ambiguousities between the underlying mathematical syntax (i.e., HOL) and the OCL level by using colors: Expressions that are internally used within HOL-OCL, like the lifting operator _ are printed in a green typeface.Using our mathematical OCL syntax, expressions on the OCL level , like _ ∧ _, are written in a magenta typeface.For the concrete syntax presented in the standard, e. g., _ and _, we use a magenta typeface.In rare cases, notable for the arithmetic operators like _ + _, we deviate from this scheme out of technical reasons.• HOL formluae are written using the usual mathematical notion, i. e., s ∈ S.Theory files for HOL-OCL and Isabelle/HOL are printed as follows:Keywords are printed in a green typeface.• SML code fragments are written inline like fn x => 2 * x or in display style: datatype OclType = Integer | Real | String | Boolean | OclAny | Set of OclType (* ... *)Keywords are printed in a blue typeface.Further, we mark problems and extensions to the OCL standard as follows:• Errors in the standard are marked by with a danger sign on the margin throughout Glitch this document, and our definitions can be seen as our proposal for repair.• In some cases we see our proposals as an extension of the standard, these cases are marked with an exclamation sign on the margin.