# Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

Achim D. Brucker, Frédéric Tuong, Burkhart Wolff

► To cite this version:

Achim D. Brucker, Frédéric Tuong, Burkhart Wolff. Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. 15th International Workshop on OCL and Textual Modeling co-located with 18th International Conference on Model Driven Engineering Languages and Systems, Oct 2015, Karlsruhe, Germany. pp.199. [hal-01213440](https://hal.inria.fr/HAL-01213440)

HAL Id: hal-01213440

https://inria.hal.science/hal-01213440

Submitted on 11 Oct 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Featherweight OCL

## A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

Achim D. Brucker*

Frédéric Tuong†‡

Burkhart Wolff†‡

October 11, 2015

*SAP SE

Vincenz-Priessnitz-Str. 1, 76131 Karlsruhe, Germany

achim.brucker@sap.com

†LRI, Univ. Paris-Sud, CNRS, CentraleSupélec, Université Paris-Saclay

bât. 650 Ada Lovelace, 91405 Orsay, France

frederic.tuong@lri.fr

burkhart.wolff@lri.fr

‡IRT SystemX

8 av. de la Vauve, 91120 Palaiseau, France

frederic.tuong@irt-systemx.fr

burkhart.wolff@irt-systemx.fr
<figure><img src="image_2.png" /></figure>
Abstract

The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in
industry. While UML is mostly known as diagrammatic modeling language (e. g., visualizing class
models), it is complemented by a textual language, called Object Constraint Language (OCL). OCL is
a textual annotation language, originally based on a three-valued logic, that turns UML into a formal
language. Unfortunately the semantics of this specification language, captured in the “Annex A” of the
OCL standard, leads to different interpretations of corner cases. Many of these corner cases had been
subject to formal analysis since more than ten years.

The situation complicated with the arrival of version 2.3 of the OCL standard. OCL was aligned
with the latest version of UML: this led to the extension of the three-valued logic by a second exception
element, called null. While the first exception element invalid has a strict semantics, null has a
non strict interpretation. The combination of these semantic features lead to remarkable confusion for
implementors of OCL compilers and interpreters.

In this paper, we provide a formalization of the core of OCL in HOL. It provides denotational
definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by
a mixture of term rewriting and code compilation. Moreover, we describe a coding-scheme for UML
class models that were annotated by code-invariants and code contracts. An implementation of this
coding-scheme has been undertaken: it consists of a kind of compiler that takes a UML class model
and translates it into a family of definitions and derived theorems over them capturing the properties
of constructors and selectors, tests and casts resulting from the class model. However, this compiler is
not included in this document.

Our formalization reveals several inconsistencies and contradictions in the current version of the OCL
standard. They reflect a challenge to define and implement OCL tools in a uniform manner. Overall,
this document is intended to provide the basis for a machine-checked text “Annex A” of the OCL
standard targeting at tool implementors.
<figure><img src="image_3.png" /></figure>
# Contents

<table><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>I.</td><td>Formal Semantics of OCL</td><td>13</td></tr><tr><td>0.1.</td><td>Introduction</td><td>15</td></tr><tr><td>0.2.</td><td>Background</td><td>18</td></tr><tr><td>0.2.1.</td><td>A Running Example for UML/OCL</td><td>18</td></tr><tr><td>0.2.2.</td><td>Formal Foundation</td><td>20</td></tr><tr><td></td><td>A Gentle Introduction to Isabelle</td><td>20</td></tr><tr><td></td><td>Higher-order Logic (HOL)</td><td>22</td></tr><tr><td>0.2.3.</td><td>How this Annex A was Generated from Isabelle/HOL Theories</td><td>24</td></tr><tr><td>0.3.</td><td>The Essence of UML-OCL Semantics</td><td>25</td></tr><tr><td>0.3.1.</td><td>The Theory Organization</td><td>25</td></tr><tr><td>0.3.2.</td><td>Denotational Semantics of Types</td><td>25</td></tr><tr><td>0.3.3.</td><td>Denotational Semantics of Constants and Operations</td><td>26</td></tr><tr><td>0.3.4.</td><td>Logical Layer</td><td>28</td></tr><tr><td>0.3.5.</td><td>Algebraic Layer</td><td>29</td></tr><tr><td>0.3.6.</td><td>Object-oriented Datatype Theories</td><td>31</td></tr><tr><td></td><td>A Denotational Space for Class-Models: Object Universes</td><td>32</td></tr><tr><td></td><td>Denotational Semantics of Accessors on Objects and Associations</td><td>33</td></tr><tr><td></td><td>Logic Properties of Class-Models</td><td>35</td></tr><tr><td></td><td>Algebraic Properties of the Class-Models</td><td>36</td></tr><tr><td></td><td>Other Operations on States</td><td>36</td></tr><tr><td>0.3.7.</td><td>Data Invariants</td><td>37</td></tr><tr><td>0.3.8.</td><td>Operation Contracts</td><td>37</td></tr><tr><td>1.</td><td>Formalization I: OCL Types and Core Definitions</td><td>39</td></tr><tr><td>1.1.</td><td>Preliminaries</td><td>39</td></tr><tr><td>1.1.1.</td><td>Notations for the Option Type</td><td>39</td></tr><tr><td>1.1.2.</td><td>Common Infrastructure for all OCL Types</td><td>39</td></tr><tr><td>1.1.3.</td><td>Accommodation of Basic Types to the Abstract Interface</td><td>40</td></tr><tr><td>1.1.4.</td><td>The Common Infrastructure of Object Types (Class Types) and States.</td><td>41</td></tr><tr><td>1.1.5.</td><td>Common Infrastructure for all OCL Types (II): Valuations as OCL Types</td><td>41</td></tr><tr><td>1.1.6.</td><td>The fundamental constants 'invalid' and 'null' in all OCL Types</td><td>42</td></tr><tr><td>1.2.</td><td>Basic OCL Value Types</td><td>42</td></tr><tr><td>1.3.</td><td>Some OCL Collection Types</td><td>43</td></tr><tr><td>1.3.1.</td><td>The Construction of the Pair Type (Tuples)</td><td>43</td></tr><tr><td>1.3.2.</td><td>The Construction of the Set Type</td><td>44</td></tr><tr><td>1.3.3.</td><td>The Construction of the Bag Type</td><td>44</td></tr><tr><td>1.3.4.</td><td>The Construction of the Sequence Type</td><td>45</td></tr><tr><td>1.3.5.</td><td>Discussion: The Representation of UML/OCL Types in Featherweight OCL</td><td>45</td></tr><tr><td>2.</td><td>Formalization II: OCL Terms and Library Operations</td><td>47</td></tr><tr><td>2.1.</td><td>The Operations of the Boolean Type and the OCL Logic</td><td>47</td></tr><tr><td>2.1.1.</td><td>Basic Constants</td><td>47</td></tr><tr><td>2.1.2.</td><td>Validity and Definedness</td><td>47</td></tr></tbody></table>
<table>
  <tbody>
    <tr>
      <td>2.1.3.</td>
      <td>The Equalities of OCL</td>
      <td>49</td>
    </tr>
    <tr>
      <td></td>
      <td>Definition</td>
      <td>50</td>
    </tr>
    <tr>
      <td></td>
      <td>Fundamental Predicates on Strong Equality</td>
      <td>50</td>
    </tr>
    <tr>
      <td>2.1.4.</td>
      <td>Logical Connectives and their Universal Properties</td>
      <td>51</td>
    </tr>
    <tr>
      <td>2.1.5.</td>
      <td>A Standard Logical Calculus for OCL</td>
      <td>55</td>
    </tr>
    <tr>
      <td></td>
      <td>Global vs. Local Judgements</td>
      <td>55</td>
    </tr>
    <tr>
      <td></td>
      <td>Local Validity and Meta-logic</td>
      <td>56</td>
    </tr>
    <tr>
      <td></td>
      <td>Local Judgements and Strong Equality</td>
      <td>59</td>
    </tr>
    <tr>
      <td>2.1.6.</td>
      <td>OCL's if then else endif</td>
      <td>60</td>
    </tr>
    <tr>
      <td>2.1.7.</td>
      <td>Fundamental Predicates on Basic Types: Strict (Referential) Equality</td>
      <td>61</td>
    </tr>
    <tr>
      <td>2.1.8.</td>
      <td>Laws to Establish Definedness (δ-closure)</td>
      <td>61</td>
    </tr>
    <tr>
      <td>2.1.9.</td>
      <td>A Side-calculus for Constant Terms</td>
      <td>62</td>
    </tr>
    <tr>
      <td>2.2.</td>
      <td>Property Profiles for OCL Operators via Isabelle Locales</td>
      <td>64</td>
    </tr>
    <tr>
      <td>2.2.1.</td>
      <td>Property Profiles for Monadic Operators</td>
      <td>64</td>
    </tr>
    <tr>
      <td>2.2.2.</td>
      <td>Property Profiles for Single</td>
      <td>65</td>
    </tr>
    <tr>
      <td>2.2.3.</td>
      <td>Property Profiles for Binary Operators</td>
      <td>65</td>
    </tr>
    <tr>
      <td>2.2.4.</td>
      <td>Fundamental Predicates on Basic Types: Strict (Referential) Equality</td>
      <td>68</td>
    </tr>
    <tr>
      <td>2.2.5.</td>
      <td>Test Statements on Boolean Operations</td>
      <td>69</td>
    </tr>
    <tr>
      <td>2.3.</td>
      <td>Basic Type Void: Operations</td>
      <td>69</td>
    </tr>
    <tr>
      <td>2.3.1.</td>
      <td>Fundamental Properties on Voids: Strict Equality</td>
      <td>70</td>
    </tr>
    <tr>
      <td></td>
      <td>Definition</td>
      <td>70</td>
    </tr>
    <tr>
      <td>2.3.2.</td>
      <td>Basic Void Constants</td>
      <td>70</td>
    </tr>
    <tr>
      <td>2.3.3.</td>
      <td>Validity and Definedness Properties</td>
      <td>70</td>
    </tr>
    <tr>
      <td>2.3.4.</td>
      <td>Test Statements</td>
      <td>70</td>
    </tr>
    <tr>
      <td>2.4.</td>
      <td>Basic Type Integer: Operations</td>
      <td>71</td>
    </tr>
    <tr>
      <td>2.4.1.</td>
      <td>Fundamental Predicates on Integers: Strict Equality</td>
      <td>71</td>
    </tr>
    <tr>
      <td>2.4.2.</td>
      <td>Basic Integer Constants</td>
      <td>71</td>
    </tr>
    <tr>
      <td>2.4.3.</td>
      <td>Validity and Definedness Properties</td>
      <td>71</td>
    </tr>
    <tr>
      <td>2.4.4.</td>
      <td>Arithmetical Operations</td>
      <td>72</td>
    </tr>
    <tr>
      <td></td>
      <td>Definition</td>
      <td>72</td>
    </tr>
    <tr>
      <td></td>
      <td>Basic Properties</td>
      <td>73</td>
    </tr>
    <tr>
      <td></td>
      <td>Execution with Invalid or Null or Zero as Argument</td>
      <td>73</td>
    </tr>
    <tr>
      <td>2.4.5.</td>
      <td>Test Statements</td>
      <td>73</td>
    </tr>
    <tr>
      <td>2.5.</td>
      <td>Basic Type Real: Operations</td>
      <td>74</td>
    </tr>
    <tr>
      <td>2.5.1.</td>
      <td>Fundamental Predicates on Reals: Strict Equality</td>
      <td>74</td>
    </tr>
    <tr>
      <td>2.5.2.</td>
      <td>Basic Real Constants</td>
      <td>75</td>
    </tr>
    <tr>
      <td>2.5.3.</td>
      <td>Validity and Definedness Properties</td>
      <td>75</td>
    </tr>
    <tr>
      <td>2.5.4.</td>
      <td>Arithmetical Operations</td>
      <td>75</td>
    </tr>
    <tr>
      <td></td>
      <td>Definition</td>
      <td>75</td>
    </tr>
    <tr>
      <td></td>
      <td>Basic Properties</td>
      <td>76</td>
    </tr>
    <tr>
      <td></td>
      <td>Execution with Invalid or Null or Zero as Argument</td>
      <td>77</td>
    </tr>
    <tr>
      <td>2.5.5.</td>
      <td>Test Statements</td>
      <td>77</td>
    </tr>
    <tr>
      <td>2.6.</td>
      <td>Basic Type String: Operations</td>
      <td>78</td>
    </tr>
    <tr>
      <td>2.6.1.</td>
      <td>Fundamental Properties on Strings: Strict Equality</td>
      <td>78</td>
    </tr>
    <tr>
      <td>2.6.2.</td>
      <td>Basic String Constants</td>
      <td>78</td>
    </tr>
    <tr>
      <td>2.6.3.</td>
      <td>Validity and Definedness Properties</td>
      <td>78</td>
    </tr>
    <tr>
      <td>2.6.4.</td>
      <td>String Operations</td>
      <td>79</td>
    </tr>
    <tr>
      <td></td>
      <td>Definition</td>
      <td>79</td>
    </tr>
    <tr>
      <td></td>
      <td>Basic Properties</td>
      <td>79</td>
    </tr>
    <tr>
      <td>2.6.5.</td>
      <td>Test Statements</td>
      <td>79</td>
    </tr>
    <tr>
      <td>2.7.</td>
      <td>Collection Type Pairs: Operations</td>
      <td>80</td>
    </tr>
    <tr>
      <td>2.7.1.</td>
      <td>Semantic Properties of the Type Constructor</td>
      <td>80</td>
    </tr>
    <tr>
      <td>2.7.2.</td>
      <td>Fundamental Properties of Strict Equality</td>
      <td>80</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>2.7.3. Standard Operations Definitions</td>
      <td>80</td>
    </tr>
    <tr>
      <td>Definition: Pair Constructor</td>
      <td>81</td>
    </tr>
    <tr>
      <td>Definition: First</td>
      <td>81</td>
    </tr>
    <tr>
      <td>Definition: Second</td>
      <td>81</td>
    </tr>
    <tr>
      <td>2.7.4. Logical Properties</td>
      <td>81</td>
    </tr>
    <tr>
      <td>2.7.5. Algebraic Execution Properties</td>
      <td>81</td>
    </tr>
    <tr>
      <td>2.7.6. Test Statements</td>
      <td>81</td>
    </tr>
    <tr>
      <td>2.8. Collection Type Bag: Operations</td>
      <td>82</td>
    </tr>
    <tr>
      <td>2.8.1. As a Motivation for the (infinite) Type Construction: Type-Extensions as Bags</td>
      <td>82</td>
    </tr>
    <tr>
      <td>2.8.2. Basic Properties of the Bag Type</td>
      <td>84</td>
    </tr>
    <tr>
      <td>2.8.3. Definition: Strict Equality</td>
      <td>84</td>
    </tr>
    <tr>
      <td>2.8.4. Constants: mtBag</td>
      <td>85</td>
    </tr>
    <tr>
      <td>2.8.5. Definition: Including</td>
      <td>85</td>
    </tr>
    <tr>
      <td>2.8.6. Definition: Excluding</td>
      <td>85</td>
    </tr>
    <tr>
      <td>2.8.7. Definition: Includes</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.8. Definition: Excludes</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.9. Definition: Size</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.10. Definition: IsEmpty</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.11. Definition: NotEmpty</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.12. Definition: Any</td>
      <td>86</td>
    </tr>
    <tr>
      <td>2.8.13. Definition: Forall</td>
      <td>87</td>
    </tr>
    <tr>
      <td>2.8.14. Definition: Exists</td>
      <td>87</td>
    </tr>
    <tr>
      <td>2.8.15. Definition: Iterate</td>
      <td>87</td>
    </tr>
    <tr>
      <td>2.8.16. Definition: Select</td>
      <td>87</td>
    </tr>
    <tr>
      <td>2.8.17. Definition: Reject</td>
      <td>88</td>
    </tr>
    <tr>
      <td>2.8.18. Definition: IncludesAll</td>
      <td>88</td>
    </tr>
    <tr>
      <td>2.8.19. Definition: ExcludesAll</td>
      <td>88</td>
    </tr>
    <tr>
      <td>2.8.20. Definition: Union</td>
      <td>88</td>
    </tr>
    <tr>
      <td>2.8.21. Definition: Intersection</td>
      <td>88</td>
    </tr>
    <tr>
      <td>2.8.22. Definition: Count</td>
      <td>89</td>
    </tr>
    <tr>
      <td>2.8.23. Definition (future operators)</td>
      <td>89</td>
    </tr>
    <tr>
      <td>2.8.24. Test Statements</td>
      <td>89</td>
    </tr>
    <tr>
      <td>2.9. Collection Type Set: Operations</td>
      <td>90</td>
    </tr>
    <tr>
      <td>2.9.1. As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets</td>
      <td>90</td>
    </tr>
    <tr>
      <td>2.9.2. Basic Properties of the Set Type</td>
      <td>91</td>
    </tr>
    <tr>
      <td>2.9.3. Definition: Strict Equality</td>
      <td>92</td>
    </tr>
    <tr>
      <td>2.9.4. Constants: mtSet</td>
      <td>92</td>
    </tr>
    <tr>
      <td>2.9.5. Definition: Including</td>
      <td>93</td>
    </tr>
    <tr>
      <td>2.9.6. Definition: Excluding</td>
      <td>93</td>
    </tr>
    <tr>
      <td>2.9.7. Definition: Includes</td>
      <td>93</td>
    </tr>
    <tr>
      <td>2.9.8. Definition: Excludes</td>
      <td>93</td>
    </tr>
    <tr>
      <td>2.9.9. Definition: Size</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.10. Definition: IsEmpty</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.11. Definition: NotEmpty</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.12. Definition: Any</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.13. Definition: Forall</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.14. Definition: Exists</td>
      <td>94</td>
    </tr>
    <tr>
      <td>2.9.15. Definition: Iterate</td>
      <td>95</td>
    </tr>
    <tr>
      <td>2.9.16. Definition: Select</td>
      <td>95</td>
    </tr>
    <tr>
      <td>2.9.17. Definition: Reject</td>
      <td>95</td>
    </tr>
    <tr>
      <td>2.9.18. Definition: IncludesAll</td>
      <td>95</td>
    </tr>
    <tr>
      <td>2.9.19. Definition: ExcludesAll</td>
      <td>95</td>
    </tr>
    <tr>
      <td>2.9.20. Definition: Union</td>
      <td>96</td>
    </tr>
  </tbody>
</table>
<table>
  <tbody>
    <tr>
      <td>2.9.21. Definition: Intersection</td>
      <td>96</td>
    </tr>
    <tr>
      <td>2.9.22. Definition (future operators)</td>
      <td>96</td>
    </tr>
    <tr>
      <td>2.9.23. Logical Properties</td>
      <td>96</td>
    </tr>
    <tr>
      <td>2.9.24. Execution Laws with Invalid or Null or Infinite Set as Argument</td>
      <td>98</td>
    </tr>
    <tr>
      <td>Context Passing</td>
      <td>100</td>
    </tr>
    <tr>
      <td>Const</td>
      <td>101</td>
    </tr>
    <tr>
      <td>2.9.25. General Algebraic Execution Rules</td>
      <td>101</td>
    </tr>
    <tr>
      <td>Execution Rules on Including</td>
      <td>101</td>
    </tr>
    <tr>
      <td>Execution Rules on Excluding</td>
      <td>102</td>
    </tr>
    <tr>
      <td>Execution Rules on Includes</td>
      <td>104</td>
    </tr>
    <tr>
      <td>Execution Rules on Excludes</td>
      <td>105</td>
    </tr>
    <tr>
      <td>Execution Rules on Size</td>
      <td>105</td>
    </tr>
    <tr>
      <td>Execution Rules on IsEmpty</td>
      <td>105</td>
    </tr>
    <tr>
      <td>Execution Rules on NotEmpty</td>
      <td>105</td>
    </tr>
    <tr>
      <td>Execution Rules on Any</td>
      <td>106</td>
    </tr>
    <tr>
      <td>Execution Rules on Forall</td>
      <td>106</td>
    </tr>
    <tr>
      <td>Execution Rules on Exists</td>
      <td>106</td>
    </tr>
    <tr>
      <td>Execution Rules on Iterate</td>
      <td>106</td>
    </tr>
    <tr>
      <td>Execution Rules on Select</td>
      <td>107</td>
    </tr>
    <tr>
      <td>Execution Rules on Reject</td>
      <td>107</td>
    </tr>
    <tr>
      <td>Execution Rules Combining Previous Operators</td>
      <td>107</td>
    </tr>
    <tr>
      <td>2.9.26. Test Statements</td>
      <td>109</td>
    </tr>
    <tr>
      <td>2.10. Collection Type Sequence: Operations</td>
      <td>110</td>
    </tr>
    <tr>
      <td>2.10.1. Basic Properties of the Sequence Type</td>
      <td>110</td>
    </tr>
    <tr>
      <td>2.10.2. Definition: Strict Equality</td>
      <td>110</td>
    </tr>
    <tr>
      <td>2.10.3. Constants: mtSequence</td>
      <td>111</td>
    </tr>
    <tr>
      <td>2.10.4. Definition: Prepend</td>
      <td>111</td>
    </tr>
    <tr>
      <td>2.10.5. Definition: Including</td>
      <td>111</td>
    </tr>
    <tr>
      <td>2.10.6. Definition: Excluding</td>
      <td>112</td>
    </tr>
    <tr>
      <td>2.10.7. Definition: Append</td>
      <td>112</td>
    </tr>
    <tr>
      <td>2.10.8. Definition: Union</td>
      <td>112</td>
    </tr>
    <tr>
      <td>2.10.9. Definition: At</td>
      <td>112</td>
    </tr>
    <tr>
      <td>2.10.10. Definition: First</td>
      <td>112</td>
    </tr>
    <tr>
      <td>2.10.11. Definition: Last</td>
      <td>113</td>
    </tr>
    <tr>
      <td>2.10.12. Definition: Iterate</td>
      <td>113</td>
    </tr>
    <tr>
      <td>2.10.13. Definition: Forall</td>
      <td>113</td>
    </tr>
    <tr>
      <td>2.10.14. Definition: Exists</td>
      <td>113</td>
    </tr>
    <tr>
      <td>2.10.15. Definition: Collect</td>
      <td>113</td>
    </tr>
    <tr>
      <td>2.10.16. Definition: Select</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.17. Definition: Size</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.18. Definition: IsEmpty</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.19. Definition: NotEmpty</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.20. Definition: Any</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.21. Definition (future operators)</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.22. Logical Properties</td>
      <td>114</td>
    </tr>
    <tr>
      <td>2.10.23. Execution Laws with Invalid or Null as Argument</td>
      <td>114</td>
    </tr>
    <tr>
      <td>Context Passing</td>
      <td>115</td>
    </tr>
    <tr>
      <td>Const</td>
      <td>115</td>
    </tr>
    <tr>
      <td>2.10.24. General Algebraic Execution Rules</td>
      <td>115</td>
    </tr>
    <tr>
      <td>Execution Rules on Iterate</td>
      <td>115</td>
    </tr>
    <tr>
      <td>2.10.25. Test Statements</td>
      <td>115</td>
    </tr>
    <tr>
      <td>2.11. Miscellaneous Stuff</td>
      <td>116</td>
    </tr>
    <tr>
      <td>2.11.1. Definition: asBoolean</td>
      <td>116</td>
    </tr>
  </tbody>
</table>
<table><tr><td>2.11.2. Definition: asInteger</td><td>116</td></tr><tr><td>2.11.3. Definition: asReal</td><td>117</td></tr><tr><td>2.11.4. Definition: asPair</td><td>117</td></tr><tr><td>2.11.5. Definition: asSet</td><td>117</td></tr><tr><td>2.11.6. Definition: asSequence</td><td>118</td></tr><tr><td>2.11.7. Definition: asBag</td><td>118</td></tr><tr><td>2.11.8. Collection Types</td><td>118</td></tr><tr><td>2.11.9. Test Statements</td><td>118</td></tr></table>

### 3. Formalization III: UML/OCL constructs: State Operations and Objects 121

3.1. Introduction: States over Typed Object Universes 121

3.1.1. Fundamental Properties on Objects: Core Referential Equality 121
Definition 121
Strictness and context passing 121

3.1.2. Logic and Algebraic Layer on Object 122
Validity and Definedness Properties 122
Symmetry 122
Behavior vs StrongEq 122

3.2. Operations on Object 123

3.2.1. Initial States (for testing and code generation) 123

3.2.2. OclAllInstances 123
OclAllInstances (@post) 125
OclAllInstances (@pre) 127
@post or @pre 128

3.2.3. OclIsNew, OclIsDeleted, OclIsMaintained, OclIsAbsent 128

3.2.4. OclIsModifiedOnly 129
Definition 129
Execution with Invalid or Null or Null Element as Argument 129
Context Passing 130

3.2.5. OclSelf 130

3.2.6. Framing Theorem 130

3.2.7. Miscellaneous 131

3.3. Accessors on Object 131

3.3.1. Definition 131

3.3.2. Validity and Definedness Properties 131

### 4. Example: The Employee Analysis Model 141

4.1. Introduction 141

4.1.1. Outlining the Example 141

4.2. Example Data-Universe and its Infrastructure 142

4.3. Instantiation of the Generic Strict Equality 143

4.4. OclAsType 143

4.4.1. Definition 143

4.4.2. Context Passing 144

4.4.3. Execution with Invalid or Null as Argument 144

4.5. OclIsTypeOf 145

4.5.1. Definition 145

4.5.2. Context Passing 146

4.5.3. Execution with Invalid or Null as Argument 146

4.5.4. Up Down Casting 147

4.6. OclIsKindOf 147

4.6.1. Definition 147

4.6.2. Context Passing 148
<table><tbody><tr><td>4.6.3.</td><td>Execution with Invalid or Null as Argument</td><td>148</td></tr><tr><td>4.6.4.</td><td>Up Down Casting</td><td>149</td></tr><tr><td>4.7.</td><td>OclAllInstances</td><td>149</td></tr><tr><td>4.7.1.</td><td>OclIsTypeOf</td><td>149</td></tr><tr><td>4.7.2.</td><td>OclIsKindOf</td><td>150</td></tr><tr><td>4.8.</td><td>The Accessors (any, boss, salary)</td><td>151</td></tr><tr><td>4.8.1.</td><td>Definition (of the association Employee-Boss)</td><td>151</td></tr><tr><td>4.8.2.</td><td>Context Passing</td><td>153</td></tr><tr><td>4.8.3.</td><td>Execution with Invalid or Null as Argument</td><td>154</td></tr><tr><td>4.8.4.</td><td>Representation in States</td><td>154</td></tr><tr><td>4.9.</td><td>A Little Infra-structure on Example States</td><td>155</td></tr><tr><td>4.10.</td><td>OCL Part: Invariant</td><td>159</td></tr><tr><td>4.11.</td><td>OCL Part: The Contract of a Recursive Query</td><td>160</td></tr><tr><td>4.12.</td><td>OCL Part: The Contract of a User-defined Method</td><td>161</td></tr><tr><td><b>5.</b></td><td><b>Example: The Employee Design Model</b></td><td><b>163</b></td></tr><tr><td>5.1.</td><td>Introduction</td><td>163</td></tr><tr><td>5.1.1.</td><td>Outlining the Example</td><td>163</td></tr><tr><td>5.2.</td><td>Example Data-Universe and its Infrastructure</td><td>163</td></tr><tr><td>5.3.</td><td>Instantiation of the Generic Strict Equality</td><td>164</td></tr><tr><td>5.4.</td><td>OclAsType</td><td>165</td></tr><tr><td>5.4.1.</td><td>Definition</td><td>165</td></tr><tr><td>5.4.2.</td><td>Context Passing</td><td>166</td></tr><tr><td>5.4.3.</td><td>Execution with Invalid or Null as Argument</td><td>166</td></tr><tr><td>5.5.</td><td>OclIsTypeOf</td><td>167</td></tr><tr><td>5.5.1.</td><td>Definition</td><td>167</td></tr><tr><td>5.5.2.</td><td>Context Passing</td><td>167</td></tr><tr><td>5.5.3.</td><td>Execution with Invalid or Null as Argument</td><td>168</td></tr><tr><td>5.5.4.</td><td>Up Down Casting</td><td>169</td></tr><tr><td>5.6.</td><td>OclIsKindOf</td><td>169</td></tr><tr><td>5.6.1.</td><td>Definition</td><td>169</td></tr><tr><td>5.6.2.</td><td>Context Passing</td><td>170</td></tr><tr><td>5.6.3.</td><td>Execution with Invalid or Null as Argument</td><td>170</td></tr><tr><td>5.6.4.</td><td>Up Down Casting</td><td>171</td></tr><tr><td>5.7.</td><td>OclAllInstances</td><td>171</td></tr><tr><td>5.7.1.</td><td>OclIsTypeOf</td><td>171</td></tr><tr><td>5.7.2.</td><td>OclIsKindOf</td><td>172</td></tr><tr><td>5.8.</td><td>The Accessors (any, boss, salary)</td><td>173</td></tr><tr><td>5.8.1.</td><td>Definition</td><td>173</td></tr><tr><td>5.8.2.</td><td>Context Passing</td><td>174</td></tr><tr><td>5.8.3.</td><td>Execution with Invalid or Null as Argument</td><td>175</td></tr><tr><td>5.8.4.</td><td>Representation in States</td><td>176</td></tr><tr><td>5.9.</td><td>A Little Infra-structure on Example States</td><td>176</td></tr><tr><td>5.10.</td><td>OCL Part: Invariant</td><td>180</td></tr><tr><td>5.11.</td><td>OCL Part: The Contract of a Recursive Query</td><td>182</td></tr></tbody></table>

## II. Conclusion 183

### 6. Conclusion 185

6.1. Lessons Learned and Contributions 185

6.2. Lessons Learned 186

6.3. Conclusion and Future Work 186
III. Appendix 193

A. The OCL And Featherweight OCL Syntax 195
<figure><img src="image_4.png" /></figure>
# Part I.

## Formal Semantics of OCL
<figure><img src="image_5.png" /></figure>
## 0.1. Introduction

The Unified Modeling Language (UML) [30, 31] is one of the few modeling languages that is widely used in industry. UML is defined in an open process by the Object Management Group (OMG), i. e., an industry consortium. While UML is mostly known as diagrammatic modeling language (e. g., visualizing class models), it also comprises a textual language, called Object Constraint Language (OCL) [32]. OCL is a textual annotation language, originally conceived as a three-valued logic, that turns substantial parts of UML into a formal language. Unfortunately the semantics of this specification language, captured in the “Annex A” (originally, based on the work of Richters [33]) of the OCL standard leads to different interpretations of corner cases. Many of these corner cases had been subject to formal analysis since more than nearly fifteen years (see, e. g., [5, 10, 18, 22, 26]).

At its origins [28, 33], OCL was conceived as a strict semantics for undefinedness (e. g., denoted by the element invalid<fnref n="1" />), with the exception of the logical connectives of type Boolean that constitute a three-valued propositional logic. At its core, OCL comprises four layers:

1. Operators (e. g., `_, and`, `_, + _`) on built-in data structures such as Boolean, Integer, or typed sets (`Set(_)`.

2. Operators on the user-defined data model (e. g., defined as part of a UML class model) such as accessors, type casts and tests.

3. Arbitrary, user-defined, side-effect-free methods called *queries*,

4. Specification for invariants on states and contracts for operations to be specified via pre- and post-conditions.

Motivated by the need for aligning OCL closer with UML, recent versions of the OCL standard [29, 32] added a second exception element. While the first exception element invalid has a strict semantics, null has a non strict semantic interpretation. Unfortunately, this extension results in several inconsistencies and contradictions. These problems are reflected in difficulties to define interpreters, code-generators, specification animators or theorem provers for OCL in a uniform manner and resulting incompatibilities of various tools.

For the OCL community, the semantics of invalid and null as well as many related issues resulted in the challenge to define a consistent version of the OCL standard that is well aligned with the recent developments of the UML. A syntactical and semantical consistent standard requires a major revision of both the informal and formal parts of the standard. To discuss the future directions of the standard, several OCL experts met in November 2013 in Aachen to discuss possible mid-term improvements of OCL, strategies of standardization of OCL within the OMG, and a vision for possible long-term developments of the language [14]. During this meeting, a Request for Proposals (RFP) for OCL 2.5 was finalized and meanwhile proposed. In particular, this RFP requires that the future OCL 2.5 standard document shall be generated from a machine-checked source. This will ensure

* the absence of syntax errors,

* the consistency of the formal semantics,

* a suite of corner-cases relevant for OCL tool implementors.

In this document, we present a formalization using Isabelle/HOL [27] of a core language of OCL. The semantic theory, based on a “shallow embedding”, is called Featherweight OCL, since it focuses on a formal treatment of the key-elements of the language (rather than a full treatment of all operators and thus, a “complete” implementation). In contrast to full OCL, it comprises just the logic captured in Boolean, the basic data types Integer, Real and String, the collection types Set, Sequence and Bag, as well as the generic construction principle of class models, which is instantiated and demonstrated for two examples (an automated support for this type-safe construction is out of the scope of Featherweight

<footnote n="1">¹In earlier versions of the OCL standard, this element was called *OclUndefined*.</footnote>
OCL). This formal semantics definition is intended to be a proposal for the standardization process of OCL 2.5, which should ultimately replace parts of the mandatory part of the standard document [32] as well as replace completely its informative "Annex A."

The semantic definitions are in large parts executable, in some parts only provable, namely the essence of Set-and Bag-constructions. The first goal of its construction is consistency, i. e., it should be possible to apply logical rules and/or evaluation rules for OCL in an arbitrary manner always yielding the same result. Moreover, except in pathological cases, this result should be unambiguously defined, i. e., represent a value.

To motivate the need for logical consistency and also the magnitude of the problem, we focus on one particular feature of the language as example: **Tuples**. Recall that tuples (in other languages known as *records*) are *n*-ary Cartesian products with named components, where the component names are used also as projection functions: the special case `Pair{x:First, y:Second}` stands for the usual binary pairing operator `Pair{true, null}` and the two projection functions `x.First()` and `x.Second()`. For a developer of a compiler or proof-tool (based on, say, a connection to an SMT solver designed to animate OCL contracts) it would be natural to add the rules `Pair{X,Y}.First() = X` and `Pair{X,Y}.Second() = Y` to give pairings the usual semantics. At some place, the OCL Standard requires the existence of a constant symbol `invalid` and requires all operators to be strict. To implement this, the developer might be tempted to add a generator for corresponding strictness axioms, producing among hundreds of other rules `Pair{invalid,Y}=invalid`, `Pair{X,invalid}=invalid`, `invalid.First()=invalid`, `invalid.Second()=invalid`, etc. Unfortunately, this "natural" axiomatization of pairing and projection together with strictness is already inconsistent. One can derive:

Pair{true, invalid}.First() = invalid.First() = invalid

and:

Pair{true, invalid}.First() = true

which then results in the absurd logical consequence that `invalid = true`. Obviously, we need to be more careful on the side-conditions of our rules<fnref n="2" />. And obviously, only a mechanized check of these definitions, following a rigorous methodology, can establish strong guarantees for logical consistency of the OCL language.

This leads us to our second goal of this document: it should not only be usable by logicians, but also by developers of compilers and proof-tools. For this end, we *derived* from the Isabelle definitions also *logical rules* allowing formal interactive and automated proofs on UML/OCL specifications, as well as *execution rules* and *test-cases* revealing corner-cases resulting from this semantics which give vital information for the implementor.

OCL is an annotation language for UML models, in particular class models allowing for specifying data and operations on them. As such, it is a *typed object-oriented language*. This means that it is—like Java or C++—based on the concept of a *static type*, that is the type that the type-checker infers from a UML class model and its OCL annotation, as well as a *dynamic type*, that is the type at which an object is dynamically created<fnref n="3" />. Types are not only a means for efficient compilation and a support of separation of concerns in programming, there are of fundamental importance for our goal of logical consistency: it is impossible to have sets that contain themselves, i. e., to state Russels Paradox in OCL typed set-theory. Moreover, object-oriented typing means that types there can be in sub-typing relation; technically speaking, this means that they can be *cast* via `oclIsTypeOf(T)` one to the other, and under particular conditions to be described in detail later, these casts are semantically *lossless*, i. e.,

$$ (X.oclAsType(C_j).oclAsType(C_i) = X) \qquad (0.1) $$

(where $C_j$ and $C_i$ are class types.) Furthermore, object-oriented means that operations and object-types can be grouped to *classes* on which an inheritance relation can be established; the latter induces a sub-type relation between the corresponding types.

<footnote n="2">²The solution to this little riddle can be found in Section 2.7.</footnote>

<footnote n="3">³As side-effect free language, OCL has no object-constructors, but with `OclIsNew()`, the effect of object creation can be expressed in a declarative way.</footnote>
Here is a feature-list of Featherweight OCL:

* it specifies key built-in types such as *Boolean*, *Void*, *Integer*, *Real* and *String* as well as generic types such as `Pair(T, T')`, `Sequence(T)` and `Set(T)`.

* it defines the semantics of the operations of these types in *denotational form*—see explanation below—, and thus in an unambiguous (and in Isabelle/HOL executable or animatable) way.

* it develops the *theory* of these definitions, i. e., the collection of lemmas and theorems that can be proven from these definitions.

* all types in Featherweight OCL contain the elements `null` and `invalid`; since this extends to *Boolean* type, this results in a four-valued logic. Consequently, Featherweight OCL contains the derivation of the *logic* of OCL.

* collection types may contain `null` (so `Set{null}` is a defined set) but not `invalid` (`Set{invalid}` is just `invalid`).

* Wrt. to the static types, Featherweight OCL is a strongly typed language in the Hindley-Milner tradition. We assume that a pre-process for full OCL eliminates all implicit conversions due to subtyping by introducing explicit casts (e. g., `oclAsType(Class)`).<fnref n="4" />

* Featherweight OCL types may be arbitrarily nested. For example, the expression `Set{Set{1,2}} = Set{Set{2,1}}` is legal and true.

* Featherweight OCL types may be higher-order nested. For example, the expression `\<lambda> X. Set{X} = Set{Set{2,1}}` is legal. Higher-order pattern-matching can be easily extended following the principles in the HOL library, which can be applied also to Featherweight OCL types.

* All objects types are represented in an object universe<fnref n="5" />. The universe construction also gives semantics to type casts, dynamic type tests, as well as functions such as `allInstances()`, or `oclIsNew()`. The object universe construction is conceptually described and demonstrated at an example.

* As part of the OCL logic, Featherweight OCL develops the theory of equality in UML/OCL. This includes the standard equality, which is a computable strict equality using the object references for comparison, and the not necessarily computable logical equality, which expresses the Leibniz principle that 'equals may be replaced by equals' in OCL terms.

* Technically, Featherweight OCL is a *semantic embedding* into a powerful semantic meta-language and environment, namely Isabelle/HOL [27]. It is a so-called *shallow embedding* in HOL; this means that types in OCL were mapped one-to-one to types in Isabelle/HOL. Ill-typed OCL specifications can therefore not be represented in Featherweight OCL and a type in Featherweight OCL contains exactly the values that are possible in OCL.

**Context.** This document stands in a more than fifteen years tradition of giving a formal semantics to the core of UML and its annotation language OCL, starting from Richters [33] and [18, 22, 26], leading to a number of formal, machine-checked versions, most notably HOL-OCL [4, 6, 7, 10] and more recent approaches [15]. All of them have in common the attempt to reconcile the conflicting demands of an industrially used specification language and its various stakeholders, the needs of OMG standardization process and the desire for sufficient logical precision for tool-implementors, in particular from the Formal Methods research community. To discuss the future directions of the standard, several OCL experts met in November 2013 in Aachen to discuss possible mid-term improvements of OCL, strategies of

<footnote n="4">⁴The details of such a pre-processing are described in [4].</footnote>

<footnote n="5">⁵following the tradition of HOL-OCL [7]</footnote>
<figure><img src="image_6.png" /><figcaption>Figure 0.1.: A simple UML class model representing a conference system for organizing conference sessions: persons can participate, in different roles, in a session.</figcaption></figure>

standardization of OCL within the OMG, and a vision for possible long-term developments of the language [14]. The participants agreed that future proposals for a formal semantics should be machine-check, to ensure the absence of syntax errors, the consistency of the formal semantics, as well as provide a suite of corner-cases relevant for OCL tool implementors.

**Organization of this document.** This document is organized as follows. After a brief background section introducing a running example and basic knowledge on Isabelle/HOL and its formal notations, we present the formal semantics of Featherweight OCL introducing:

1. A conceptual description of the formal semantics, highlighting the essentials and avoiding the definitions in detail.

2. A detailed formal description. This covers:

a) OCL Types and their presentation in Isabelle/HOL,

b) OCL Terms, i. e., the semantics of library operators, together with definitions, lemmas, and test cases for the implementor,

c) UML/OCL Constructs, i. e., a core of UML class models plus user-defined constructions on them such as class-invariants and operation contracts.

3. Since the latter, i. e., the construction of UML class models, has to be done on the meta-level (so not *inside* HOL, rather on the level of a pre-compiler), we will describe this process with two larger examples, namely formalizations of our running example.

## 0.2. Background

### 0.2.1. A Running Example for UML/OCL

The Unified Modeling Language (UML) [30, 31] comprises a variety of model types for describing static (e. g., class models, object models) and dynamic (e. g., state-machines, activity graphs) system properties. One of the more prominent model types of the UML is the *class model* (visualized as *class diagram*) for modeling the underlying data model of a system in an object-oriented manner. As a running example, we model a part of a conference management system. Such a system usually supports the conference organizing process, e. g., creating a conference Website, reviewing submissions, registering attendees, organizing the different sessions and tracks, and indexing and producing the resulting proceedings. In this example, we constrain ourselves to the process of organizing conference sessions; Figure 0.1 shows the class model. We model the hierarchy of roles of our system as a hierarchy of classes (e. g., *Hearer*, *Speaker*, or *Chair*) using an *inheritance relation* (also called *generalization*).
In particular, *inheritance* establishes a *subtyping* relationship, i.e., every **Speaker** (*subclass*) is also a **Hearer** (*superclass*).

A class does not only describe a set of *instances* (called *objects*), i.e., record-like data consisting of *attributes* such as *name* of class *Session*, but also *operations* defined over them. For example, for the class *Session*, representing a conference session, we model an operation `findRole(p:Person):Role` that should return the role of a *Person* in the context of a specific session; later, we will describe the behavior of this operation in more detail using UML. In the following, the term object describes a (run-time) instance of a class or one of its subclasses.

Relations between classes (called *associations* in UML) can be represented in a class diagram by connecting lines, e. g., **Participant** and **Session** or **Person** and **Role**. Associations may be labeled by a particular constraint called *multiplicity*, e. g., `0..*` or `0..1`, which means that in a relation between participants and sessions, each **Participant** object is associated to at most one **Session** object, while each **Session** object may be associated to arbitrarily many **Participant** objects. Furthermore, associations may be labeled by projection functions like **person** and **role**; these implicit function definitions allow for OCL-expressions like `self.person`, where `self` is a variable of the class **Role**. The expression `self.person` denotes persons being related to the specific object **self** of type **role**. A particular feature of the UML are *association classes* (**Participant** in our example) which represent a concrete tuple of the relation within a system state as an object; i. e., association classes allow also for defining attributes and operations for such tuples. In a class diagram, association classes are represented by a dotted line connecting the class with the association. Associations classes can take part in other associations. Moreover, UML supports also *n*-ary associations (not shown in our example).

We refine this data model using the Object Constraint Language (OCL) for specifying additional invariants, preconditions and postconditions of operations. For example, we specify that objects of the class **Person** are uniquely determined by the value of the *name* attribute and that the attribute *name* is not equal to the empty string (denoted by `''`):

```text
context Person
inv: name <> '' and
    Person::allInstances()->isUnique(p:Person | p.name)
```

Moreover, we specify that every session has exactly one chair by the following invariant (called `onlyOneChair`) of the class **Session**:

```text
context Session
inv onlyOneChair: self.participants->one( p:Participant |
                                           p role.oclIsTypeOf(Chair))
```

where `p role.oclIsTypeOf(Chair)` evaluates to true, if `p role` is of *dynamic type Chair*. Besides the usual *static types* (i. e., the types inferred by a static type inference), objects in UML and other object-oriented languages have a second *dynamic type concept*. This is a consequence of a family of *casting functions* (written `o[C]` for an object `o` into another class type `C`) that allows for converting the static type of objects along the class hierarchy. The dynamic type of an object can be understood as its "initial static type" and is unchanged by casts. We complete our example by describing the behavior of the operation `findRole` as follows:

```text
context Session::findRole(person:Person):Role
pre: self.participates.person->includes(person)
post: result self.participates->one(p:Participant |
                                   p.person = person ).role
and self.participates = self.participates@pre
and self.name = self.name@pre
```

where in post-conditions, the operator `@pre` allows for accessing the previous state. Note that:

```text
pre: self.participates.person->includes(person)
```

is actually a syntactic abbreviation for a constraint referring to the previous state:
self.participates@pre.person@pre->includes(person).

Note, further, that conventions for full-OCL permit the suppression of the self-parameter, following similar syntactic conventions in other object-oriented languages such as Java:

context Session::findRole(person:Person):Role
pre: participates.person->includes(person)
post: result=participants->one(p:Participant |
      p.person = person ).role
and participants = participants@pre
and name = name@pre

In UML, classes can contain attributes of the type of the defining class. Thus, UML can represent (mutually) recursive datatypes. Moreover, OCL introduces also recursively specified operations.

A key idea of defining the semantics of UML and extensions like SecureUML [11] is to translate the diagrammatic UML features into a combination of more elementary features of UML and OCL expressions [20]. For example, associations (i. e., relations on objects) can be implemented in specifications at the design level by aggregations, i. e., collection-valued class attributes together with OCL constraints expressing the multiplicity. Thus, having a semantics for a subset of UML and OCL is tantamount for the foundation of the entire method.

0.2.2. Formal Foundation

A Gentle Introduction to Isabelle

Isabelle [27] is a *generic* theorem prover. New object logics can be introduced by specifying their syntax and natural deduction inference rules. Among other logics, Isabelle supports first-order logic, Zermelo-Fraenkel set theory and the instance for Church's higher-order logic (HOL).

The core language of Isabelle is a typed λ -calculus providing a uniform term language T in which all logical entities where represented: 6

$$
T ::= C | V | \lambda V. T | T T
$$

where:

• C is the set of constant symbols like "fst" or "snd" as operators on pairs. Note that Isabelle's syntax engine supports mixfix-notation for terms: "(_ = ⇒ __) A B" or "(_ + __) A B" can be parsed and printed as "A = ⇒ B" or "A + B", respectively.

• V is the set of variable symbols like "x", "y", "z", . . . Variables standing in the scope of a λ -operator were called bound variables, all others are free variables.

• "λ V. T" is called λ -abstraction. For example, consider the identity function λ x.x. A λ -abstraction forms a scope for the variable V .

• T T ′ is called an application .

These concepts are not at all Isabelle specific and can be found in many modern programming languages ranging from Haskell over Python to Java.

Terms where associated to types by a set of type inference rules $^{7}$; only terms for which a type can be inferred—i. e., for typed terms —were considered as legal input to the Isabelle system. The type-terms τ for λ -terms are defined as: 8

$$
\tau ::= TV \mid TV ::= \Xi \mid \tau \Rightarrow \tau \mid (\tau, \dots, \tau)TC \qquad (0.2)
$$

<footnote>$^{6}$In the Isabelle implementation, there are actually two further variants which were irrelevant for this presentation and are therefore omitted.</footnote>

<footnote>$^{7}$Similar to https://en.wikipedia.org/w/index.php?title=Hindley%E2%80%93Milner_type_system&oldid=668548458</footnote>

<footnote>$^{8}$Again, the Isabelle implementation is actually slightly different; our presentation is an abstraction in order to improve readability.</footnote>
• TV is the set of *type variables* like '$\alpha, \beta, ...$'. The syntactic categories *V* and *TV* are disjoint; thus, '$x$' is a perfectly possible type variable.

• $\Xi$ is a set of *type-classes* like *ord*, *order*, *linorder*, ... This feature in the Isabelle type system is inspired by Haskell type classes.<fnref n="9" /> A *type class constraint* such as `"α :: order"` expresses that the type variable '$\alpha$' may range over any type that has the algebraic structure of a partial ordering (as it is configured in the Isabelle/HOL library).

• The type '$\alpha \Rightarrow \beta$' denotes the total function space from '$\alpha$' to '$\beta$'.

• *TC* is a set of *type constructors* like `"(\alpha) list"` or `"(\alpha) tree"`. Again, Isabelle's syntax engine supports mixfix-notation for type terms: cartesian products '$\alpha \times \beta$' or type sums '$\alpha + \beta$' are notations for `"(\alpha, \beta)(\_ \< times \> \_ )"' or `"(\alpha, \beta)(\_ + \_ )"`, respectively. Also null-ary type-constructors like `()` `bool`, `()` `nat` and `()` `int` are possible; note that the parentheses of null-ary type constructors are usually omitted.

Isabelle accepts also the notation `t :: \tau` as type assertion in the term-language; `t :: \tau` means "t is required to have type `\tau`". Note that typed terms can contain free variables; terms like `x + y = y + x` reflecting common mathematical notation (and the convention that free variables are implicitly universally quantified) are possible and common in Isabelle theories.<fnref n="10" />.

An environment providing $\Xi$, *TC* as well as a map from constant symbols *C* to types (built over these $\Xi$ and *TC*) is called a *global context*; it provides a kind of signature, i. e., a mechanism to construct the syntactic material of a logical theory.

The most basic (built-in) global context of Isabelle provides just a language to construct logical rules. More concretely, it provides a constant declaration for the (built-in) *meta-level implication* `\_ = \_` allowing to form constructs like $A_1 \Rightarrow \dots \Rightarrow A_n \Rightarrow A_{n+1}$, which are viewed as a *rule* of the form “from assumptions $A_1$ to $A_n$, infer conclusion $A_{n+1}$” and which is written in Isabelle syntax as

$$ [[A_1; \dots; A_n]] \Rightarrow A_{n+1} \quad \text{or, in mathematical notation,} \quad \frac{A_1 \quad \dots \quad A_n}{A_{n+1}}. \qquad (0.3) $$

Moreover, the built-in meta-level quantification Forall($\lambda x. E x$) (pretty-printed and parsed as $\forall x. E x$) captures the usual side-constraints “$x$ must not occur free in the assumptions” for quantifier rules; meta-quantified variables can be considered as “fresh” free variables. Meta-level quantification leads to a generalization of Horn-clauses of the form:

$$ \forall x_1, \dots, x_m. [[A_1; \dots; A_n]] \Rightarrow A_{n+1}. \qquad (0.4) $$

Isabelle supports forward- and backward reasoning on rules. For backward-reasoning, a *proof-state* can be initialized in a given global context and further transformed into others. For example, a proof of $\phi$, using the Isar [36] language, will look as follows in Isabelle:

$$ \begin{array}{l} \text{lemma label: } \phi \\ \text{apply(case\_tac)} \\ \text{apply(simp\_all)} \end{array} \qquad (0.5) $$

done

This proof script instructs Isabelle to prove $\phi$ by case distinction followed by a simplification of the resulting proof state. Such a proof state is an implicitly conjoint sequence of generalized Horn-clauses (called *subgoals*) $\phi_1, \dots, \phi_n$ and a *goal* $\phi$. Proof states were usually denoted by:

$$ \begin{array}{l} \text{label : } \phi \\ \quad 1. \phi_1 \\ \qquad \vdots \\ \quad n. \phi_n \end{array} \qquad (0.6) $$

<footnote n="9">⁹See https://en.wikipedia.org/w/index.php?title=Type_class&oldid=672053941.</footnote>

<footnote n="10">¹⁰Here, we assume that `\_ + \_` and `\_ = \_` are declared constant symbols having type `int` ⇒ `int` ⇒ `int` and `$\alpha \Rightarrow \alpha$ ⇒ bool`, respectively.</footnote>
Subgoals and goals may be extracted from the proof state into theorems of the form $[[\phi_1; \dots; \phi_n]] \Rightarrow \phi$ at any time;

By extensions of global contexts with axioms and proofs of theorems, theories can be constructed step by step. Beyond the basic mechanisms to extend a global context by a type-constructor-, type-class-constant-definition or an axiom, Isabelle offers a number of commands that allow for more complex extensions of theories in a logically safe way (avoiding the use of axioms directly).

## Higher-order Logic (HOL)

Higher-order logic (HOL) [1, 16] is a classical logic based on a simple type system. Isabelle/HOL is a theory extension of the basic Isabelle core-language with operators and the 7 axioms of HOL; together with large libraries this constitutes an implementation of HOL. Isabelle/HOL provides the usual logical connectives like `\wedge`, `\to`, `\neg` as well as the object-logical quantifiers `\forall x. P x` and `\exists x. P x`; in contrast to first-order logic, quantifiers may range over arbitrary types, including total functions `f::\alpha \Rightarrow \beta`. HOL is centered around extensional equality `=` `=`:: `\alpha \Rightarrow \alpha \Rightarrow \beta`. Extensional equality means that two functions `f` and `g` are equal if and only if they are point-wise equal; this is captured by the rule: `(\wedge x. f x = g x) \Rightarrow f = g`. HOL is more expressive than first-order logic, since, among many other things, induction schemes can be expressed inside the logic. For example, the standard induction rule on natural numbers in HOL:

$$ P 0 \Rightarrow (\wedge x. P x \Rightarrow P (x + 1)) \Rightarrow P x $$

is just an ordinary rule in Isabelle which is in fact a proven theorem in the theory of natural numbers. This example exemplifies an important design principle of Isabelle: theorems and rules are technically the same, paving the way to derived rules and automated decision procedures based on them. This has the consequence that these procedures are consequently sound by construction with respect to their logical aspects (they may be incomplete or failing, though).

On the other hand, Isabelle/HOL can also be viewed as a functional programming language like SML or Haskell. Isabelle/HOL definitions can usually be read just as another functional programming language; if not interested in proofs and the possibilities of a specification language providing powerful logical quantifiers or equivalent free variables, the reader can just ignore these aspects in theories.

Isabelle/HOL offers support for a particular methodology to extend given theories in a logically safe way: A theory-extension is conservative if the extended theory is consistent provided that the original theory was consistent. Conservative extensions can be constant definitions, type definitions, datatype definitions, primitive recursive definitions and well founded recursive definitions.

For instance, the library includes the type constructor `\tau_\perp` `:= \perp | \perp_\_`: `\alpha` that assigns to each type `\tau` a type `\tau_\perp` disjointly extended by the exceptional element `\perp`. The function `\top_\_`: `\alpha_\perp \to \alpha` is the inverse of `\perp_\_` (unspecified for `\perp`). Partial functions `\alpha \to \beta` are defined as functions `\alpha \Rightarrow \beta_\perp` supporting the usual concepts of domain (`dom_\_`) and range (`ran_\_`).

As another example of a conservative extension, typed sets were built in the Isabelle libraries conservatively on top of the kernel of HOL as functions to `bool`; consequently, the constant definitions for membership is as follows:<fnref n="11" />

$$
\begin{array}{lll}
\text{types} & \alpha \text{ set} = \alpha \Rightarrow \text{bool} & \\
\text{definition} & \text{Collect} \quad ::(\alpha \Rightarrow \text{bool}) \Rightarrow \alpha \text{ set} & \text{--- set comprehension} \\
\text{where} & \text{Collect } S \equiv S & (0.7) \\
\text{definition} & \text{member} \quad ::\alpha \Rightarrow \alpha \Rightarrow \text{bool} & \text{--- membership test} \\
\text{where} & \text{member } s S \equiv Ss &
\end{array}
$$

Isabelle's syntax engine is instructed to accept the notation `{x | P}` for `Collect \lambda x. P` and the notation `s \in S` for member `s S`. As can be inferred from the example, constant definitions are axioms that introduce a fresh constant symbol by some non-recursive expressions not containing free variables; this

<footnote n="11">¹¹To increase readability, we use a slightly simplified presentation.</footnote>
type of axiom is logically safe since it works like an abbreviation. The syntactic side conditions of this axiom are mechanically checked. It is straightforward to express the usual operations on sets like `_` `∪` `_` `∩` `_` `:: α` set ⇒ `α` set ⇒ `α` set as conservative extensions, too, while the rules of typed set theory were derived by proofs from these definitions.

Similarly, a logical compiler is invoked for the following statements introducing the types option and list:

$$ 
\begin{align} 
\text{datatype option} &= \text{None} \mid \text{Some } \alpha \tag{0.8} \\ 
\text{datatype } \alpha \text{ list} &= \text{Nil} \mid \text{Cons } a \ l \nonumber
\end{align} 
$$

Here, `[]` or `a#l` are an alternative syntax for `Nil` or `Cons a l`; moreover, `[a, b, c]` is defined as alternative syntax for `a#b#c#[]`. These (recursive) statements were internally represented in by internal type and constant definitions. Besides the constructors `None`, `Some`, `[]` and `Cons`, there is the match operation

$$ \text{case } x \text{ of } \text{None} \Rightarrow F \mid \text{Some } a \Rightarrow G a \tag{0.9} $$

respectively

$$ \text{case } x \text{ of } [] \Rightarrow F \mid \text{Cons } a \ r \Rightarrow G a \ r. \tag{0.10} $$

From the internal definitions (not shown here) several properties were automatically derived. We show only the case for lists:

$$ 
\begin{align*}
(\text{case } [] \text{ of } [] \Rightarrow F \mid (a\#r) \Rightarrow G a \ r) &= F \\
(\text{case } b\#t \text{ of } [] \Rightarrow F \mid (a\#r) \Rightarrow G a \ r) &= G \ b \ t \\
[] \neq a\#t &\qquad \text{– distinctness} \tag{0.11} \\
[a = [] \Rightarrow P; \exists \ t. a = x\#t \Rightarrow P] &\qquad \text{– exhaust} \\
[P []; \forall \ at. P \ t \to P(a\#t)] &\qquad \text{– induct}
\end{align*} 
$$

Finally, there is a compiler for primitive and well founded recursive function definitions. For example, we may define the sort operation on linearly ordered lists by:

$$ 
\begin{align*}
\text{fun} \quad &\text{ins} \quad \text{::}[\alpha \:: \text{inorder}, \alpha \text{ list}] \Rightarrow \alpha \text{ list} \\
\text{where} \quad &\text{ins } x \ [\ ] \quad = \ [x] \tag{0.12} \\
&\text{ins } x \ (y\#ys) \quad = \ \text{if } x < y \text{ then } x\#y\#ys \text{ else } y\#(\text{ins } x \ ys)
\end{align*} 
$$

$$ 
\begin{align*}
\text{fun} \quad &\text{sort} \quad \text{::}(\alpha \:: \text{inorder}) \text{ list} \Rightarrow \alpha \text{ list} \\
\text{where} \quad &\text{sort} \ [\ ] \quad = \ [\ ] \tag{0.13} \\
&\text{sort}(x\#xs) \quad = \text{ins } x \ (\text{sort } xs)
\end{align*} 
$$

The internal (non-recursive) constant definition for these operations is quite involved; however, the logical compiler will finally derive all the equations in the statements above from this definition and make them available for automated simplification.

Thus, Isabelle/HOL also provides a large collection of theories like sets, lists, orderings, and various arithmetic theories which only contain rules derived from conservative definitions. This library constitutes a comfortable basis for defining the OCL library and language constructs.

In particular, Isabelle manages a set of *executable types and operators*, i. e., types and operators for which a compilation to SML, OCaml or Haskell is possible. Setups for arithmetic types such as `int` have been done; moreover any `datatype` and any recursive function were included in this executable set (providing that they only consist of executable operators). This forms the basis that many OCL terms can be executed directly. Using the value command, it is possible to compile many OCL ground expressions (no free variables) to code and to execute them; for example value `"3 + 7"` just answers with 10 in Isabelle's output window. This is even true for many expressions containing types which in themselves are not executable. For example, the `Set` type, which is defined in Featherweight OCL as the type of potentially infinite sets, is consequently not in itself executable; however, due to special setups of the code-generator, expressions like value `"Set{1,2}"` are, because the underlying constructors in this expression allow for automatically establishing that this set is finite and reducible to constructs that are in this special case executable.
<figure><img src="image_7.png" /><figcaption>Figure 0.2.: Generating documents with guaranteed syntactical and semantical consistency.</figcaption></figure>

### 0.2.3. How this Annex A was Generated from Isabelle/HOL Theories

Isabelle, as a framework for building formal tools [35], provides the means for generating *formal documents*. With formal documents (such as the one you are currently reading) we refer to documents that are machine-generated and ensure certain formal guarantees. In particular, all formal content (e. g., definitions, formulae, types) are checked for consistency during the document generation.

For writing documents, Isabelle supports the embedding of informal texts using a LATEX-based markup language within the theory files. To ensure the consistency, Isabelle supports to use, within these informal texts, *antiquotations* that refer to the formal parts and that are checked while generating the actual document as PDF. For example, in an informal text, the antiquotation `@{thm "not_not"}` will instruct Isabelle to lock-up the (formally proven) theorem of name `ocl_not_not` and to replace the antiquotation with the actual theorem, i. e., `not (not x) = x`.

Figure 0.2 illustrates this approach: Figure 0.2a shows the `jEdit`-based development environment of Isabelle with an excerpt of one of the core theories of Featherweight OCL. Figure 0.2b shows the generated PDF document where all antiquotations are replaced. Moreover, the document generation tools allows for defining syntactic sugar as well as skipping technical details of the formalization.

Featherweight OCL is a formalization of the core of OCL aiming at formally investigating the relationship between the various concepts. At present, it does not attempt to define the complete OCL library. Instead, it concentrates on the core concepts of OCL as well as the types `Boolean`, `Integer`, and typed sets (`Set(T)`). Following the tradition of HOL-OCL [6, 8], Featherweight OCL is based on the following principles:

1. It is an embedding into a powerful semantic meta-language and environment, namely Isabelle/HOL [27].

2. It is a *shallow embedding* in HOL; types in OCL were injectively mapped to types in Featherweight OCL. Ill-typed OCL specifications cannot be represented in Featherweight OCL and a type in Featherweight OCL contains exactly the values that are possible in OCL. Thus, sets may contain `null` (`Set{null}` is a defined set) but not invalid (`Set{invalid}` is just invalid).

3. Any Featherweight OCL type contains at least invalid and null (the type `Void` contains only these instances). The logic is consequently four-valued, and there is a null-element in the type `Set(A)`.
4. It is a strongly typed language in the Hindley-Milner tradition. We assume that a pre-process eliminates all implicit conversions due to sub-typing by introducing explicit casts (e. g., `oc1AsType()`). The details of such a pre-processing are described in [4]. Casts are semantic functions, typically injections, that may convert data between the different Featherweight OCL types.

5. All objects are represented in an object universe in the HOL-OCL tradition [7]. The universe construction also gives semantics to type casts, dynamic type tests, as well as functions such as `oc1AllInstances()`, or `oc1IsNew()`.

6. Featherweight OCL types may be arbitrarily nested. For example, the expression `Set{Set{1,2}} = Set{Set{2,1}}` is legal and true.

7. For demonstration purposes, the set type in Featherweight OCL may be infinite, allowing infinite quantification and a constant that contains the set of all Integers. Arithmetic laws like commutativity may therefore be expressed in OCL itself. The iterator is only defined on finite sets.

8. It supports equational reasoning and congruence reasoning, but this requires a differentiation of the different equalities like strict equality, strong equality, meta-equality (HOL). Strict equality and strong equality require a sub-calculus, "cp" (a detailed discussion of the different equalities as well as the sub-calculus "cp"-for three-valued OCL 2.0-is given in [9]), which is nasty but can be hidden from the user inside tools.

Overall, this would contribute to one of the main goals of the OCL 2.5 RFP, as discussed at the OCL meeting in Aachen [14].

## 0.3. The Essence of UML-OCL Semantics

### 0.3.1. The Theory Organization

The semantic theory is organized in a quite conventional manner in three layers. The first layer, called the *denotational semantics* comprises a set of definitions of the operators of the language. Presented as *definitional axioms* inside Isabelle/HOL, this part assures the logically consistency of the overall construction. The denotational definitions of types, constants and operations, and OCL contracts represent the “gold standard” of the semantics. The second layer, called *logical layer*, is derived from the former and centered around the notion of validity of an OCL formula *P*. For a state-transition from pre-state $\sigma$ to post-state $\sigma'$, a validity statement is written $(\sigma, \sigma') \models P$. Its major purpose is to logically establish facts (lemmas and theorems) about the denotational definitions. The third layer, called *algebraic layer*, also derived from the former layers, tries to establish algebraic laws of the form $P = P'$; such laws are amenable to equational reasoning and also help for automated reasoning and code-generation. For an implementor of an OCL compiler, these consequences are of most interest.

For space reasons, we will restrict ourselves in this document to a few operators and make a traversal through all three layers to give a high-level description of our formalization. Especially, the details of the semantic construction for sets and the handling of objects and object universes were excluded from a presentation here.

### 0.3.2. Denotational Semantics of Types

The syntactic material for type expressions, called `TYPES(C)`, is inductively defined as follows:

* $C \subseteq \text{TYPES}(C)$

* Boolean, Integer, Real, Void, ... are elements of `TYPES(C)`

* `Set(X)`, `Bag(X)`, `Sequence(X)`, and `Pair(X, Y)` (as example for a Tuple-type) are in `TYPES(C)` (if $X, Y \in \text{TYPES}(C)$).
Types were directly represented in Featherweight OCL by types in HOL; consequently, any Featherweight OCL type must provide elements for a bottom element (also denoted $⊥$) and a null element; this is enforced in Isabelle by a type-class null that contains two distinguishable elements bot and null (see Chapter 1 for the details of the construction).

Moreover, the representation mapping from OCL types to Featherweight OCL is one-to-one (i. e., injective), and the corresponding Featherweight OCL types were constructed to represent *exactly* the elements ("no junk, no confusion elements") of their OCL counterparts. The corresponding Featherweight OCL types were constructed in two stages: First, a *base type* is constructed whose carrier set contains exactly the elements of the OCL type. Secondly, this base type is lifted to a *valuation type* that we use for type-checking Featherweight OCL constants, operations, and expressions. The valuation type takes into account that some UML-OCL functions of its OCL type (namely: accessors in path-expressions) depend on a pre- and a post-state.

For most base types like `Boolean_base` or `Integer_base`, it suffices to double-lift a HOL library type:

$$ \text{type\_synonym} \quad \text{Boolean}_{\text{base}} := \text{bool}_{\perp\perp} \qquad (0.14) $$

As a consequence of this definition of the type, we have the elements $⊥, \perp, \perp, \text{true}_\perp, \text{false}_\perp$ in the carrier-set of `Boolean_base`. We can therefore use the element $⊥$ to define the generic type class element $⊥$ and $\perp$ for the generic type class null. For collection types and object types this definition is more evolved (see Chapter 1).

For object base types, we assume a typed universe $\mathfrak{A}$ of objects to be discussed later, for the moment we will refer it by its polymorphic variable.

With respect the valuation types for OCL expression in general and Boolean expressions in particular, they depend on the pair $(\sigma, \sigma')$ of pre-and post-state. Thus, we define valuation types by the synonym:

$$ \text{type\_synonym} \quad V_{\mathfrak{A}}(\alpha) := \text{state}(\mathfrak{A}) \times \text{state}(\mathfrak{A}) \to \alpha \:: \text{null}. \qquad (0.15) $$

The valuation type for boolean, integer, etc. OCL terms is therefore defined as:

$$ \begin{array}{ll} \text{type\_synonym} & \text{Boolean}_{\mathfrak{A}} := V_{\mathfrak{A}}(\text{Boolean}_{\text{base}}) \\ \text{type\_synonym} & \text{Integer}_{\mathfrak{A}} := V_{\mathfrak{A}}(\text{Integer}_{\text{base}}) \\ \dots & \dots \end{array} $$

the other cases are analogous. In the subsequent subsections, we will drop the index $\mathfrak{A}$ since it is constant in all formulas and expressions except for operations related to the object universe construction in Section 3.1

The rules of the logical layer (there are no algebraic rules related to the semantics of types), and more details can be found in Chapter 1.

### 0.3.3. Denotational Semantics of Constants and Operations

We use the notation $I[[E]]\tau$ for the semantic interpretation function as commonly used in mathematical textbooks and the variable $\tau$ standing for pairs of pre- and post state $(\sigma, \sigma')$. Note that we will also use $\tau$ to denote the type of a state-pair; since both syntactic categories are independent, we can do so without arising confusion. OCL provides for all OCL types the constants `invalid` for the exceptional computation result and `null` for the non-existing value. Thus we define:

$$ I[[\text{invalid}:: V(\alpha)]\tau \equiv \text{bot}] \quad I[[\text{null}:: V(\alpha)]\tau \equiv \text{null}] $$

For the concrete `Boolean`-type, we define similarly the boolean constants `true` and `false` as well as the fundamental tests for definedness and validity (generically defined for all types):

$$ \begin{array}{l} I[[\text{true}:: \text{Boolean}]]\tau = \perp, \text{true}_\perp \quad I[[\text{false}]]\tau = \perp, \text{false}_\perp \\ I[[X.\text{oclIsUndefined()}]]\tau = (\text{if } I[[X]]\tau \in \{\text{bot, null}\} \text{ then } I[[\text{true}]]\tau \text{ else } I[[\text{false}]]\tau) \end{array} $$
$$
I[X. \mathit{oclIsInvalid()} \rangle \tau = (\mathit{if} I[X] \tau = \mathit{bot} \ \mathit{then} I[\mathbf{true}] \tau \ \mathit{else} I[\mathbf{false}] \tau)
$$

For reasons of conciseness, we will write $\delta X$ for not($X$.oclIsUndefined()) and $\upsilon X$ for not($X$.oclIsInvalid()) throughout this document.

Due to the used style of semantic representation (a shallow embedding) I is in fact superfluous and
defined semantically as the identity $\lambda x. x$; instead of:

$$
I[\mathbf{true}::\mathbf{Boolean}]\tau = \mathbf{true}
$$

we can therefore write:

$$
\mathbf{true}::\mathbf{Boolean} = \lambda \tau . \mathbf{true}
$$

In Isabelle theories, this particular presentation of definitions paves the way for an automatic check
that the underlying equation has the form of an *axiomatic definition* and is therefore logically safe.

On this basis, one can define the core logical operators not and and as follows:

$$
\begin{align*}
I[\mathbf{not} X] \tau &= (\mathbf{case} I[X] \tau \mathbf{of} \\
&\quad \bot \quad \Rightarrow \bot \\
&\quad |\bot] \quad \Rightarrow \bot \\
&\quad |\bot x] \quad \Rightarrow \bot \neg x])
\end{align*}
$$

$$
\begin{align*}
I[X \text{ and } Y] \tau &= (\mathbf{case} I[X] \tau \text{ of} \\
&\quad \bot \quad \Rightarrow (\mathbf{case} I[Y] \tau \text{ of} \\
&\qquad \bot \quad \Rightarrow \bot \\
&\qquad |\bot] \quad \Rightarrow \bot \\
&\qquad |\bot \text{true}] \quad \Rightarrow \bot \\
&\qquad |\bot \text{false}] \quad \Rightarrow \bot \text{false}] \\
|\bot] \quad \Rightarrow (\mathbf{case} I[Y] \tau \text{ of} \\
&\quad \bot \quad \Rightarrow \bot \\
&\quad |\bot] \quad \Rightarrow \bot \\
&\quad |\bot \text{true}] \quad \Rightarrow \bot \\
&\quad |\bot \text{false}] \quad \Rightarrow \bot \text{false}] \\
|\bot \text{true}] \quad \Rightarrow (\mathbf{case} I[Y] \tau \text{ of} \\
&\quad \bot \quad \Rightarrow \bot \\
&\quad |\bot] \quad \Rightarrow \bot \\
&\quad |\bot y] \quad \Rightarrow \bot y]) \\
|\bot \text{false}] \quad \Rightarrow \bot \text{false})
\end{align*}
$$

These non-strict operations were used to define the other logical connectives in the usual classical way:
X or Y ≡ (not X) and (not Y) or X implies Y ≡ (not X) or Y.

The default semantics for an OCL library operator is strict semantics; this means that the result of
an operation *f* is invalid if one of its arguments is +invalid+ or +null+. The definition of the addition
for integers as default variant reads as follows:

$$
\begin{align*}
I[x + y]_{\tau} &= \begin{align*}
&\quad \text{if } I[\delta x]_{\tau} = I[\mathbf{true}]_{\tau} \land I[\delta y]_{\tau} = I[\mathbf{true}]_{\tau} \\
&\quad \text{then}_{\bot} \top I[x]_{\tau} \top + \top I[y]_{\tau} \top \\
&\quad \text{else } \bot
\end{align*}
$$

where the operator “+” on the left-hand side of the equation denotes the OCL addition of type
Integer ⇒ Integer ⇒ Integer while the “+” on the right-hand side of the equation of type
[int, int] ⇒ int denotes the integer-addition from the HOL library.
### 0.3.4. Logical Layer

The topmost goal of the logic for OCL is to define the validity statement:

$$ (\sigma, \sigma') \models P, $$

where $\sigma$ is the pre-state and $\sigma'$ the post-state of the underlying system and $P$ is a formula, i. e., and OCL expression of type Boolean. Informally, a formula $P$ is valid if and only if its evaluation in $(\sigma, \sigma')$ (i. e., $\tau$ for short) yields true. Formally this means:

$$ \tau \models P \equiv (I[[P]]\tau = \underset{\perp}{\text{true}}_{\perp}). $$

On this basis, classical, two-valued inference rules can be established for reasoning over the logical connectives, the different notions of equality, definedness and validity. Generally speaking, rules over logical validity can relate bits and pieces in various OCL terms and allow—via strong logical equality discussed below—the replacement of semantically equivalent sub-expressions. The core inference rules are:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\tau \models \mathbf{true} & \neg(\tau \models \mathbf{false}) & \neg(\tau \models \mathbf{invalid}) & \neg(\tau \models \mathbf{null}) \\
\multicolumn{4}{l}{\tau \models \mathbf{not} P \implies \neg(\tau \models P)} \\
\multicolumn{4}{l}{\tau \models P \text{ and } Q \implies \tau \models P} & \tau \models P \text{ and } Q \implies \tau \models Q \\
\multicolumn{4}{l}{\tau \models P \implies \tau \models P \text{ or } Q} & \tau \models Q \implies \tau \models P \text{ or } Q \\
\multicolumn{4}{l}{\tau \models P \implies (\text{if } P \text{ then } B_1 \text{ else } B_2 \text{ endif}) \tau = B_1 \tau} \\
\multicolumn{4}{l}{\tau \models \mathbf{not} P \implies (\text{if } P \text{ then } B_1 \text{ else } B_2 \text{ endif}) \tau = B_2 \tau} \\
\multicolumn{4}{l}{\tau \models P \implies \tau \models \delta P} & \tau \models \delta X \implies \tau \models \upsilon X
\end{array}
$$

By the latter two properties it can be inferred that any valid property $P$ (so for example: a valid invariant) is defined, which allows to infer for terms composed by strict operations that their arguments and finally the variables occurring in it are valid or defined.

The mandatory part of the OCL standard refers to an equality (written $x = y$ or $x <> y$ for its negation), which is intended to be a strict operation (thus: invalid = y evaluates to invalid) and which uses the references of objects in a state when comparing objects, similarly to C++ or Java. In order to avoid confusions, we will use the following notations for equality:

1. The symbol `=` remains to be reserved to the HOL equality, i. e., the equality of our semantic meta-language,

2. The symbol `~` will be used for the strong logical equality, which follows the general logical principle that “equals can be replaced by equals,”<fnref n="12" /> and is at the heart of the OCL logic,

3. The symbol `:=` is used for the strict referential equality, i. e., the equality the mandatory part of the OCL standard refers to by the `_` `-` symbol.

The strong logical equality is a polymorphic concept which is defined using polymorphism for all OCL types by:

$$ I[[X \triangleq Y]]\tau \equiv \underset{\perp}{I[[X]]\tau} = I[[Y]]\tau_{\perp} $$

It enjoys nearly the laws of a congruence:

$$
\begin{align*}
\tau \models (x \triangleq x) \\
\tau \models (x \triangleq y) &\implies \tau \models (y \triangleq x) \\
\tau \models (x \triangleq y) &\implies \tau \models (y \triangleq z) \implies \tau \models (x \triangleq z) \\
cp P \implies \tau \models (x \triangleq y) &\implies \tau \models (P x) \implies \tau \models (P y)
\end{align*}
$$

<footnote n="12">¹²Strong logical equality is also referred as “Leibniz”-equality.</footnote>
where the predicate cp stands for *context-passing*, a property that is true for all pure OCL expressions (but not arbitrary mixtures of OCL and HOL) in Featherweight OCL. The necessary side-calculus for establishing cp can be fully automated; the reader interested in the details is referred to Section 2.1.3.

The strong logical equality of Featherweight OCL give rise to a number of further rules and derived properties, that clarify the role of strong logical equality and the Boolean constants in OCL specifications:

$$ 
\begin{align*}
\tau \models \delta x \lor \tau \models x \triangleq \mathbf{invalid} \lor \tau \models x \triangleq \mathbf{null}, \\
(\tau \models A \triangleq \mathbf{invalid}) &= (\tau \models \mathbf{not}(vA)) \\
(\tau \models A \triangleq \mathbf{true}) &= (\tau \models A) \qquad (\tau \models A \triangleq \mathbf{false}) = (\tau \models \mathbf{not}A) \\
(\tau \models \mathbf{not}(\delta x)) &= (\neg \tau \models \delta x) \qquad (\tau \models \mathbf{not}(vx)) = (\neg \tau \models vx)
\end{align*}
$$

The logical layer of the Featherweight OCL rules gives also a means to convert an OCL formula living in its four-valued world into a representation that is classically two-valued and can be processed by standard SMT solvers such as CVC3 [2] or Z3 [19]. $\delta$-closure rules for all logical connectives have the following format, e. g.:

$$ 
\begin{align*}
\tau \models \delta x &\implies (\tau \models \mathbf{not} x) = (\neg (\tau \models x)) \\
\tau \models \delta x &\implies \tau \models \delta y \implies (\tau \models x \ \mathbf{and} \ y) = (\tau \models x \land \tau \models y) \\
\tau \models \delta x &\implies \tau \models \delta y \\
&\implies (\tau \models (x \ \mathbf{implies} \ y)) = ((\tau \models x) \longrightarrow (\tau \models y))
\end{align*}
$$

Together with the already mentioned general case-distinction

$$ \tau \models \delta x \lor \tau \models x \triangleq \mathbf{invalid} \lor \tau \models x \triangleq \mathbf{null} $$

which is possible for any OCL type, a case distinction on the variables in a formula can be performed; due to strictness rules, formulae containing somewhere a variable $x$ that is known to be **invalid** or **null** reduce usually quickly to contradictions. For example, we can infer from an invariant $\tau \models x \doteq y - 3$ that we have $\tau \models x \doteq y - 3 \land \tau \models \delta x \land \tau \models \delta y$. We call the latter formula the $\delta$-closure of the former. Now, we can convert a formula like $\tau \models x > 0 \ or \ 3 * y > x * x$ into the equivalent formula $\tau \models x > 0 \lor \tau \models 3 * y > x * x$ and thus internalize the OCL-logic into a classical (and more tool-conform) logic. This works—for the price of a potential, but due to the usually “rich” $\delta$-closures of invariants rare—exponential blow-up of the formula for all OCL formulas.

### 0.3.5. Algebraic Layer

Based on the logical layer, we build a system with simpler rules which are amenable to automated reasoning. We restrict ourselves to pure equations on OCL expressions.

Our denotational definitions on **not** and **and** can be re-formulated in the following ground equations:

$$ 
\begin{align*}
v \ \mathbf{invalid} &= \mathbf{false} & v \ \mathbf{null} &= \mathbf{true} \\
v \ \mathbf{true} &= \mathbf{true} & v \ \mathbf{false} &= \mathbf{true} \\
\delta \ \mathbf{invalid} &= \mathbf{false} & \delta \ \mathbf{null} &= \mathbf{false} \\
\delta \ \mathbf{true} &= \mathbf{true} & \delta \ \mathbf{false} &= \mathbf{true} \\
\mathbf{not} \ \mathbf{invalid} &= \mathbf{invalid} & \mathbf{not} \ \mathbf{null} &= \mathbf{null} \\
\mathbf{not} \ \mathbf{true} &= \mathbf{false} & \mathbf{not} \ \mathbf{false} &= \mathbf{true} \\
(\mathbf{null} \ \mathbf{and} \ \mathbf{true}) &= \mathbf{null} & (\mathbf{null} \ \mathbf{and} \ \mathbf{false}) &= \mathbf{false} \\
(\mathbf{null} \ \mathbf{and} \ \mathbf{null}) &= \mathbf{null} & (\mathbf{null} \ \mathbf{and} \ \mathbf{invalid}) &= \mathbf{invalid} \\
(\mathbf{false} \ \mathbf{and} \ \mathbf{true}) &= \mathbf{false} & (\mathbf{false} \ \mathbf{and} \ \mathbf{false}) &= \mathbf{false} \\
(\mathbf{false} \ \mathbf{and} \ \mathbf{null}) &= \mathbf{false} & (\mathbf{false} \ \mathbf{and} \ \mathbf{invalid}) &= \mathbf{false}
\end{align*}
$$
$$
\begin{align*}
(\text{true and true}) &= \text{true} & (\text{true and false}) &= \text{false} \\
(\text{true and null}) &= \text{null} & (\text{true and invalid}) &= \text{invalid} \\
(\text{invalid and true}) &= \text{invalid} & (\text{invalid and false}) &= \text{false} \\
(\text{invalid and null}) &= \text{invalid} & (\text{invalid and invalid}) &= \text{invalid}
\end{align*}
$$

On this core, the structure of a conventional lattice arises:

$$
\begin{align*}
\begin{array}{l}
\text{X and } X = X \\
\text{false and } X = \text{false} \\
\text{true and } X = X
\end{array}
&
\begin{array}{l}
\text{X and } Y = Y \text{ and } X \\
\text{X and false} = \text{false} \\
\text{X and true} = X
\end{array} \\
\text{X and (Y and } Z) &= \text{X and } Y \text{ and } Z
\end{align*}
$$

as well as the dual equalities for _ or _ and the De Morgan rules. This wealth of algebraic properties makes the understanding of the logic easier as well as automated analysis possible: for example, it allows for computing a DNF of invariant systems (by term-rewriting techniques) which are a prerequisite for δ-closures.

The above equations explain the behavior for the most-important non-strict operations. The clarification of the exceptional behaviors is of key-importance for a semantic definition of the standard and the major deviation point from HOL-OCL [6, 8] to Featherweight OCL as presented here. Expressed in algebraic equations, “strictness-principles” boil down to:

$$
\begin{align*}
\text{invalid} + X &= \text{invalid} & X + \text{invalid} &= \text{invalid} \\
\text{invalid-}\rightarrow\text{including}(X) &= \text{invalid} & \text{null-}\rightarrow\text{including}(X) &= \text{invalid} \\
X \doteq \text{invalid} &= \text{invalid} & \text{invalid} \doteq X &= \text{invalid} \\
\text{S-}\rightarrow\text{including}(\text{invalid}) &= \text{invalid} & & \\
X \doteq X &= (\text{if } v \ x \ \text{then } \text{true} \ \text{else} \ \text{invalid } \ \text{endif}) & & \\
1 / 0 &= \text{invalid} & 1 / \text{null} &= \text{invalid} \\
\text{invalid-}\rightarrow\text{}(\text{ empty }) &= \text{invalid} & \text{null-}\rightarrow\text{阅}(\text{ empty }) &= \text{null}
\end{align*}
$$

Algebraic rules are also the key for execution and compilation of Featherweight OCL expressions. We derived, e. g.:

$$
\begin{align*}
\delta \text{Set}\{\} &= \text{true} \\
\delta (X \rightarrow \text{including}(x)) &= \delta X \text{ and } v x \\
\text{Set}\{\} \rightarrow \text{includes}(x) &= (\text{if } v x \text{ then } \text{false} \\
&\phantom{\text{if } v x \text{ then }} \text{else invalid } \text{endif}) \\
(X \rightarrow \text{including}(x) \rightarrow \text{includes}(y)) &= \\
&\quad (\text{if } \delta X \\
&\quad \quad \text{then } \text{if } x \doteq y \\
&\quad \quad \quad \text{then true} \\
&\quad \quad \quad \text{else } X \rightarrow \text{includes}(y) \\
&\quad \quad \quad \text{endif} \\
&\quad \quad \text{else invalid} \\
&\quad \quad \text{endif})
\end{align*}
$$

As Set{1,2} is only syntactic sugar for

Set{}->including(1)->including(2)
an expression like `Set{1,2}->includes(null)` becomes decidable in Featherweight OCL by applying these algebraic laws (which can give rise to efficient compilations). The reader interested in the list of "test-statements" like:

value "τ |= (Set{Set{2, null}} = Set{Set{null, 2}})"

make consult Section 2.9; these test-statements have been machine-checked and proven consistent with the denotational and logic semantics of Featherweight OCL.

### 0.3.6. Object-oriented Datatype Theories

In the following, we will refine the concepts of a user-defined data-model implied by a *class-model* (*visualized* by a *diagram*) as well as the notion of state used in the previous section to much more detail. UML class models represent in a compact and visual manner quite complex, object-oriented data-types with a surprisingly rich theory. In this section, this theory is made explicit and corner cases were pointed out.

A UML class model underlying a given OCL invariant or operation contract produces several implicit operations which become accessible via appropriate OCL syntax. A class model is a four-tuple (`C`, `_` < `_`, `Attrib`, `Assoc`) where:

1. `C` is a set of class names (written as `{C₁, ..., Cₙ}`). To each class name a type of data in OCL is associated. Moreover, class names declare two projector functions to the set of all objects in a state: `Cᵢ`.allInstances() and `Cᵢ`.allInstances@pre()`,

2. `_` < `_` is an inheritance relation on classes,

3. `Attrib(Cᵢ)` is a collection of attributes associated to classes `Cᵢ`. It declares two families of accessors; for each attribute `a` ∈ `Attrib(Cᵢ)` in a class definition `Cᵢ` (denoted `X.a:: Cᵢ → A` and `X.a@pre:: Cᵢ → A` for `A ∈ TYPES(C)`),

4. `Assoc(Cᵢ, Cⱼ)` is a collection of associations<fnref n="13" />. An association `(n, rnfrom, rnto) ∈ Assoc(Cᵢ, Cⱼ)` between to classes `Cᵢ` and `Cⱼ` is a triple consisting of a (unique) association name `n`, and the role-names `rnfrom` and `rnto`. To each role-name belong two families of accessors denoted `X.a:: Cᵢ → A` and `X.a@pre:: Cᵢ → A` for `A ∈ TYPES(C)`),

5. for each pair `Cᵢ < Cⱼ` (`Cᵢ, Cⱼ < C`), there is a cast operation of type `Cⱼ → Cᵢ` that can change the static type of an object of type `Cᵢ`: `obj:: Cᵢ`.oclAsType(Cⱼ)`,

6. for each class `Cᵢ ∈ C`, there are two dynamic type tests (`X.oclIsTypeOf(Cᵢ)` and `X.oclIsKindOf(Cᵢ)`),

7. and last but not least, for each class name `Cᵢ ∈ C` there is an instance of the overloaded referential equality (written `_ = _`).

Assuming a strong static type discipline in the sense of Hindley-Milner types, Featherweight OCL has no "syntactic subtyping." In contrast, sub-typing can be expressed *semantically* in Featherweight OCL by adding suitable type-casts which do have a formal semantics. Thus, sub-typing becomes an issue of the front-end that can make implicit type-coercions explicit. Our perspective shifts the emphasis on the semantic properties of casting, and the necessary universe of object representations (induced by a class model) that allows to establish them.

As a pre-requisite of a denotational semantics for these operations induced by a class-model, we need an *object-universe* in which these operations can be defined in a denotational manner and from which the necessary properties for constructors, accessors, tests and casts can be derived. A concrete universe constructed from a class model will be used to instantiate the implicit type parameter `A` of all OCL operations discussed so far.

<footnote n="13">¹³Given the fact that there is at present no consensus on the semantics of n-ary associations, Featherweight OCL restricts itself to binary associations.</footnote>
## A Denotational Space for Class-Models: Object Universes

It is natural to construct system states by a set of partial functions $f$ that map object identifiers oid to some representations of objects:

$$ \texttt{typedef } \mathfrak{A} \texttt{ state := } \{\sigma :: \texttt{oid} \to \alpha | \text{inv}_{\sigma}(\sigma)\} \qquad (0.16) $$

where $inv_{\sigma}$ is a to be discussed invariant on states.

The key point is that we need a common type $\mathfrak{A}$ for the set of all possible *object representations*. Object representations model “a piece of typed memory,” i. e., a kind of record comprising administration information and the information for all attributes of an object; here, the primitive types as well as collections over them are stored directly in the object representations, class types and collections over them are represented by oid’s (respectively lifted collections over them).

In a shallow embedding which must represent UML types one-to-one by HOL types, there are two fundamentally different ways to construct such a set of object representations, which we call an *object universe* $\mathfrak{A}$:

1. an object universe can be constructed from a given class model, leading to *closed world semantics*, and

2. an object universe can be constructed for a given class model and all its extensions by new classes added into the leaves of the class hierarchy, leading to an *open world semantics*.

For the sake of simplicity, the present semantics chose the first option for Featherweight OCL, while HOL-OCL [7] used an involved construction allowing the latter.

A naïve attempt to construct $\mathfrak{A}$ would look like this: the class type $C_i$ induced by a class will be the type of such an object representation: $C_i := (\text{oid} \times A_{i_1} \times \dots \times A_{i_k})$ where the types $A_{i_1}, \dots, A_{i_k}$ are the attribute types (including inherited attributes) with class types substituted by oid. The function $\text{OidOf}$ projects the first component, the oid, out of an object representation. Then the object universe will be constructed by the type definition:

$$ \mathfrak{A} := C_1 + \dots + C_n. \qquad (0.17) $$

It is possible to define constructors, accessors, and the referential equality on this object universe. However, the treatment of type casts and type tests cannot be faithful with common object-oriented semantics, be it in UML or Java: casting up along the class hierarchy can only be implemented by loosening information, such that casting up and casting down will *not* give the required identity, whenever $C_k < C_i$ and $X$ is valid:

$$ X.\text{oclIsTypeOf}(C_k) \text{ implies } X.\text{oclAsType}(C_i).\text{oclAsType}(C_k) = X \qquad (0.18) $$

To overcome this limitation, we introduce an auxiliary type $C_{iext}$ for *class type extension*; together, they were inductively defined for a given class diagram:

Let $C_i$ be a class with a possibly empty set of subclasses $\{C_{j_1}, \dots, C_{j_m}\}$.

* Then the *class type extension* $C_{iext}$ associated to $C_i$ is $A_{i_1} \times \dots \times A_{i_n} \times (C_{j_1ext} + \dots + C_{j_mext})_{\perp}$ where $A_{i_k}$ ranges over the local attribute types of $C_i$ and $C_{j_1ext}$ ranges over all class type extensions of the subclass $C_j$ of $C_i$.

* Then the *class type* for $C_i$ is $\text{oid} \times A_{i_1} \times \dots \times A_{i_n} \times (C_{j_1ext} + \dots + C_{j_mext})_{\perp}$ where $A_{i_k}$ ranges over the inherited and local attribute types of $C_i$ and $C_{j_1ext}$ ranges over all class type extensions of the subclass $C_j$ of $C_i$.

Example instances of this scheme—outlining a compiler—can be found in Chapter 4 and Chapter 5.

This construction can *not* be done in HOL itself since it involves quantifications and iterations over the “set of class-types”; rather, it is a meta-level construction. Technically, this means that we need a compiler to be done in SML on the syntactic “meta-model”-level of a class model.

With respect to our semantic construction here, which above all means is intended to be type-safe, this has the following consequences:
* there is a generic theory of states, which must be formulated independently from a concrete object universe,

* there is a principle of translation (captured by the inductive scheme for class type extensions and class types above) that converts a given class model into a concrete object universe,

* there are fixed principles that allow to derive the semantic theory of any concrete object universe, called the *object-oriented datatype theory*.

We will work out concrete examples for the construction of the object-universes in Chapter 4 and Chapter 5 and the derivation of the respective datatype theories. While an automatization is clearly possible and desirable for concrete applications of Featherweight OCL, we consider this out of the scope of this document which has a focus on the semantic construction and its presentation.

## Denotational Semantics of Accessors on Objects and Associations

Our choice to use a shallow embedding of OCL in HOL and, thus having an injective mapping from OCL types to HOL types, results in type-safety of Featherweight OCL. Arguments and results of accessors are based on type-safe object representations and *not* oid's. This implies the following scheme for an accessor:

* The *evaluation and extraction* phase. If the argument evaluation results in an object representation, the oid is extracted, if not, exceptional cases like *invalid* are reported.

* The *de-referentiation* phase. The oid is interpreted in the pre- or post-state, the resulting object is cast to the expected format. The exceptional case of non-existence in this state must be treated.

* The *selection* phase. The corresponding attribute is extracted from the object representation.

* The *re-construction* phase. The resulting value has to be embedded in the adequate HOL type. If an attribute has the type of an object (not value), it is represented by an optional (set of) oid, which must be converted via de-referentiation in one of the states to produce an object representation again. The exceptional case of non-existence in this state must be treated.

The first phase directly translates into the following formalization:

definition

$$ \text{eval\_extract } X \ f = (\lambda \ \tau. \ \text{case } X \ \tau \ \text{of} \quad \begin{array}{lcl} \bot & \Rightarrow & \text{invalid } \tau \\ \llcorner \urcorner & \Rightarrow & \text{invalid } \tau \\ \urcorner obj \urcorner & \Rightarrow & f(\text{oid\_of } obj) \tau \end{array} \quad \text{exception} \\ \text{deref. null} \quad (0.19) $$

For each class *C*, we introduce the de-referentiation phase of this form:

definition deref_oidC fst_snd f oid = (λτ. case (heap (fst_snd τ)) oid of

$$ \begin{array}{lcl} \llcorner \text{in}_C obj \urcorner & \Rightarrow & f obj \tau \\ \_ & \Rightarrow & \text{invalid } \tau \end{array} \quad (0.20) $$

The operation yields undefined if the oid is uninterpretable in the state or referencing an object representation not conforming to the expected type.

We turn to the selection phase: for each class *C* in the class model with at least one attribute, and each attribute *a* in this class, we introduce the selection phase of this form:

$$ \text{definition select}_a f = (\lambda mk_C \ \text{oid} \ \dots \bot \ \dots C_{X\text{ext}} \Rightarrow \text{null} \\ \mid mk_C \ \text{oid} \ \dots \llcorner a \urcorner \ \dots C_{X\text{ext}} \Rightarrow f(\lambda x \_. \llcorner x \urcorner) a) \quad (0.21) $$
null is not counted. On the other hand, the operation **size** defined for collections in OCL does count null.

We propose to resolve this dilemma by regarding multiplicities as optional. This point of view complies with the UML standard, that does not require lower and upper bounds to be defined for multiplicities.<fnref n="14" /> In case a multiplicity is specified for an attribute, i. e., a lower and an upper bound are provided, we require for any collection the attribute evaluates to a collection not containing null. This allows for a straightforward interpretation of the multiplicity constraint. If bounds are not provided for an attribute, we consider the attribute values to not be restricted in any way. Because in particular the cardinality of the attribute's values is not bounded, the result of an evaluation of the attribute is of collection type. As the range of values that the attribute can assume is not restricted, the attribute can evaluate to a collection containing null. The attribute can also evaluate to invalid. Allowing multiplicities to be optional in this way gives the modeler the freedom to define attributes that can assume the full ranges of values provided by their types. However, we do not permit the omission of multiplicities for association ends, since the values of association ends are not only restricted by multiplicities, but also by other constraints enforcing the semantics of associations. Hence, the values of association ends cannot be completely unrestricted.

**The Precise Meaning of Multiplicity Constraints** We are now ready to define the meaning of multiplicity constraints by giving equivalent invariants written in OCL. Let **a** be an attribute of a class **C** with a multiplicity specifying a lower bound **m** and an upper bound **n**. Then we can define the multiplicity constraint on the values of attribute **a** to be equivalent to the following invariants written in OCL:

context C inv lowerBound: a->size() >= m
inv upperBound: a->size() <= n
inv notNull: not a->includes(null)

If the upper bound **n** is infinite, the second invariant is omitted. For the definition of these invariants we are making use of the conversion of single values to sets described in Section 0.3.6. If $n \le 1$, the attribute **a** evaluates to a single value, which is then converted to a **Set** on which the **size** operation is called.

If a value of the attribute **a** includes a reference to a non-existent object, the attribute call evaluates to invalid. As a result, the entire expressions evaluate to invalid, and the invariants are not satisfied. Thus, references to non-existent objects are ruled out by these invariants. We believe that this result is appropriate, since we argue that the presence of such references in a system state is usually not intended and likely to be the result of an error. If the modeler wishes to allow references to non-existent objects, she can make use of the possibility described above to omit the multiplicity.

**Logic Properties of Class-Models**

In this section, we assume to be $C_z, C_i, C_j \in C$ and $C_i < C_j$. Let $C_z$ be a smallest element with respect to the class hierarchy `__<__`. The operations induced from a class-model have the following properties:

$$ 
\begin{align*}
\tau \models X.\text{oclAsType}(C_i) &\triangleq X \\
\tau \models \text{invalid} .\text{oclAsType}(C_i) &\triangleq \text{invalid} \\
\tau \models \text{null} .\text{oclAsType}(C_i) &\triangleq \text{null} \\
\tau \models ((X :: C_i) .\text{oclAsType}(C_j) .\text{oclAsType}(C_i) &\triangleq X) \\
\tau \models X.\text{oclAsType}(C_j) .\text{oclAsType}(C_i) &\triangleq X \\
\tau \models (X :: \text{OclAny}) .\text{oclAsType}(\text{OclAny}) &\triangleq X \\
\tau \models \upsilon(X :: C_i) &\implies \tau \models (X.\text{oclIsTypeOf}(C_i) \text{ implies } (X.\text{oclAsType}(C_j).\text{oclAsType}(C_i)) \doteq X)
\end{align*}
$$

<footnote n="14">¹⁴We are however aware that a well-formedness rule of the UML standard does define a default bound of one in case a lower or upper bound is not specified.</footnote>
$\tau \models \nu(X :: C_i) \implies \tau \models X.oclIsTypeOf(C_i) \text{ implies } (X.oclAsType(C_j) .oclAsType(C_i)) \doteq X$
$\tau \models \delta X \implies \tau \models X.oclAsType(C_j) .oclAsType(C_i) \triangleq X$
$\tau \models \nu X \implies \tau \models X.oclIsTypeOf(C_i) \text{ implies } X.oclAsType(C_j) .oclAsType(C_i) \doteq X$
$\tau \models X.oclIsTypeOf(C_j) \implies \tau \models \delta X \implies \tau \models \text{not}(\nu X.oclAsType(C_i))$
$\tau \models \text{invalid}.oclIsTypeOf(C_i) \triangleq \text{invalid}$
$\tau \models \text{null}.oclIsTypeOf(C_i) \triangleq \text{true}$
$\tau \models \text{Person}.allInstances() \rightarrow \text{forAll}(X|X.oclIsTypeOf(C_z))$
$\tau \models \text{Person}.allInstances@pre() \rightarrow \text{forAll}(X|X.oclIsTypeOf(C_z))$
$\tau \models \text{Person}.allInstances() \rightarrow \text{forAll}(X|X.oclIsKindOf(C_i))$
$\tau \models \text{Person}.allInstances@pre() \rightarrow \text{forAll}(X|X.oclIsKindOf(C_i))$
$\tau \models (X :: C_i).oclIsTypeOf(C_j) \implies \tau \models (X :: C_i).oclIsKindOf(C_i)$
$(\tau \models (X :: C_j) \doteq X) = (\tau \models \text{if}\nu X \text{then true else invalid endif})$
$\tau \models (X :: C_j) \doteq Y \implies \tau \models Y \doteq X$
$\tau \models (X :: C_j) \doteq Y \implies \tau \models Y \doteq Z \implies \tau \models X \doteq Z$

## Algebraic Properties of the Class-Models

In this section, we assume to be $C_i, C_j \in C$ and $C_i < C_j$. The operations induced from a class-model have the following properties:

invalid.oclIsTypeOf($C_i$) = invalid null.oclIsTypeOf($C_i$) = true
invalid.oclIsKindOf($C_i$) = invalid null.oclIsKindOf($C_i$) = true
($X :: C_i$).oclAsType($C_i$) = X invalid.oclAsType($C_i$) = invalid
null.oclAsType($C_i$) = null ($X :: C_i$).oclAsType($C_j$).oclAsType($C_i$) = X
($X :: C_i$) $\doteq$ X = \text{if}\nu X \text{then true else invalid endif}

With respect to attributes _ . a or _ . a @pre and role-ends _ . r or _ . r @pre we have

invalid.a = invalid null.a = invalid
invalid.a @pre = invalid null.a @pre = invalid
invalid.r = invalid null.r = invalid
invalid.r @pre = invalid null.r @pre = invalid

## Other Operations on States

Defining _ . allInstances() is straight-forward; the only difference is the property T . allInstances() -> excludes( null ) which is a consequence of the fact that null 's are values and do not "live" in the state. OCL semantics admits states with "dangling references,"; it is the semantics of accessors or roles which maps these references to invalid , which makes it possible to rule out these situations in invariants.

OCL does not guarantee that an operation only modifies the path-expressions mentioned in the postcondition, i. e., it allows arbitrary relations from pre-states to post-states. This framing problem is well-known (one of the suggested solutions is [23]). We define

(S: Set (OclAny)) -> oclIsModifiedOnly() : Boolean

where S is a set of object representations, encoding a set of oid's. The semantics of this operator is defined such that for any object whose oid is not represented in S and that is defined in pre and post
state, the corresponding object representation will not change in the state transition. A simplified presentation is as follows:

$$I[X \rightarrow \text{oclIsModifiedOnly}(\sigma, \sigma')](\sigma, \sigma') = \begin{cases} \perp & \text{if } X' = \perp \lor \text{null} \in X' \\ \sqsubseteq i \in M. \sigma i = \sigma' i & \text{otherwise.} \end{cases}$$

where $X' = I[X](\sigma, \sigma')$ and $M = (\text{dom } \sigma \cap \text{dom } \sigma') - \{\text{OidOf } x | x \in \Gamma X^\Gamma\}$. Thus, if we require in a postcondition $\text{Set}\}\rightarrow\text{oclIsModifiedOnly}()$ and exclude via _ . oclIsNew() and _ . oclIsDeleted()$ the existence of new or deleted objects, the operation is a query in the sense of the OCL standard, i. e., the `isQuery` property is true. So, whenever we have $\tau \models X \rightarrow \text{excluding}(s.a) \rightarrow \text{oclIsModifiedOnly}()$ and $\tau \models X \rightarrow \text{forAll}(x \text{not}|(x \doteq s.a))$, we can infer that $\tau \models s.a \triangleq s.a @ \text{pre}$.

### 0.3.7. Data Invariants

Since the present OCL semantics uses one interpretation function<fnref n="15" />, we express the effect of OCL terms occurring in preconditions and invariants by a syntactic transformation _pre which replaces:

* all accessor functions _ . a from the class model $a \in \text{Attrib}(C)$ by their counterparts _ . i@pre. For example, $(\text{self} . \text{salary} > 500)_{\text{pre}}$ is transformed to $(\text{self} . \text{salary} @ \text{pre} > 500)$.

* all role accessor functions _ . rn$_{from}$ or _ . rn$_{to}$ within the class model (i. e., $(\text{id}, \text{rn$_{from}$}, \text{rn$_{to}$}) \in \text{Assoc}(C_i, C_j)$) were replaced by their counterparts _ . rn @ pre. For example, $(\text{self} . \text{boss} = \text{null})_{\text{pre}}$ is transformed to $\text{self} . \text{boss} @ \text{pre} = \text{null}$.

* The operation _ . allInstances() is also substituted by its @pre counterpart.

Thus, we formulate the semantics of the invariant specification as follows:

$$\begin{align*} I[\text{context } c : C_i \text{ inv } n : \phi(c)]\tau &\equiv \\ &\quad \tau \models (C_i . \text{allInstances()} \rightarrow \text{forall}(x|\phi(x))) \land \tag{0.25} \\ &\quad \tau \models (C_i . \text{allInstances()} \rightarrow \text{forall}(x|\phi(x)))_{\text{pre}} \end{align*}$$

Recall that expressions containing @pre constructs in invariants or preconditions are syntactically forbidden; thus, mixed forms cannot arise.

### 0.3.8. Operation Contracts

Since operations have strict semantics in OCL, we have to distinguish for a specification of an operation `op` with the arguments `a1`, ..., `an` the two cases where all arguments are valid and additionally, `self` is non-null (i. e., it must be defined), or not. In former case, a method call can be replaced by a result that satisfies the contract, in the latter case the result is invalid. This is reflected by the following definition of the contract semantics:

$$\begin{align*} I[\text{context } C \ ::\ & op(a_1, \dots, a_n) : T \\ & \text{pre } \phi(\text{self}, a_1, \dots, a_n) \\ & \text{post } \psi(\text{self}, a_1, \dots, a_n, \text{result})] \equiv \\ & \qquad \lambda s, x_1, \dots, x_n, \tau. \tag{0.26} \\ & \text{if } \tau \models \partial s \land \tau \models v x_1 \land \dots \land \tau \models v x_n \\ & \text{then } \text{SOME } \text{result.} \quad \tau \models \phi(s, x_1, \dots, x_n)_{\text{pre}} \\ & \qquad \land \tau \models \psi(s, x_1, \dots, x_n, \text{result}) \\ & \text{else } \perp \end{align*}$$

<footnote n="15">¹⁵This has been handled differently in previous versions of the Annex A.</footnote>
where SOME x. P(x) is the Hilbert-Choice Operator that chooses an arbitrary element satisfying P; if such an element does not exist, it chooses an arbitrary one<fnref n="16" />. Thus, using the Hilbert-Choice Operator, a contract can be associated to a function definition:

$$f_{op} \equiv I[\text{context } C \:: \text{op}(a_1, \dots, a_n) : T \dots] \qquad (0.27)$$

provided that neither $\phi$ nor $\psi$ contain recursive method calls of op. In the case of a query operation (i.e., $\tau$ must have the form: $(\sigma, \sigma)$, which means that query operations do not change the state; c.f. oclIsModifiedOnly() in Section 0.3.6), this constraint can be relaxed: the above equation is then stated as axiom. Note however, that the consistency of the overall theory is for recursive query contracts left to the user (it can be shown, for example, by a proof of termination, i.e., by showing that all recursive calls were applied to argument vectors that are smaller wrt. a well-founded ordering). Under this condition, an $f_{op}$ resulting from recursive query operations can be used safely inside pre- and post-conditions of other contracts.

For the general case of a user-defined contract, the following rule can be established that reduces the proof of a property E over a method call $f_{op}$ to a proof of $E(res)$ (where res must be one of the values that satisfy the post-condition $\psi$):

$$\frac{[\tau \vdash \psi \ self \ a_1 \dots a_n \ res]_{res} \\ \vdots \\ \tau \vdash E(res) \\ \hline \tau \vdash E(f_{op} \ self \ a_1 \dots a_n)}{(0.28) \qquad \tau \vdash E(res) \qquad \tau \vdash E(f_{op} \ self \ a_1 \dots a_n)}$$

under the conditions:

* E must be an OCL term and

* self must be defined, and the arguments valid in $\tau$:
  $\tau \vdash \partial \ self \wedge \tau \vdash \psi a_1 \wedge \dots \wedge \tau \vdash \psi a_n$

* the post-condition must be satisfiable ("the operation must be implementable"): $\exists res. \tau \vdash \psi self a_1 \dots a_n res$.

For the special case of a (recursive) query method, this rule can be specialized to the following executable "unfolding principle":

$$\frac{\tau \vdash \phi \ self \ a_1 \dots a_n}{(\tau \vdash E(f_{op} \ self \ a_1 \dots a_n)) = e(\tau \vdash E(BODY \ self \ a_1 \dots a_n))} \qquad (0.29)$$

where

* E must be an OCL term.

* self must be defined, and the arguments valid in $\tau$:
  $\tau \vdash \partial \ self \wedge \tau \vdash \psi a_1 \wedge \dots \wedge \tau \vdash \psi a_n$

* the postcondition $\psi self a_1 \dots a_n result$ must be decomposable into:
  $\psi' self a_1 \dots a_n$ and $result \triangleq BODY self a_1 \dots a_n$.

Currently, Featherweight OCL neither supports overloading nor overriding for user-defined operations: the Featherweight OCL compiler needs to be extended to generate pre-conditions that constrain the classes on which an overridden function can be called as well as the dispatch order. This construction, overall, is similar to the virtual function table that, e.g., is generated by C++ compilers. Moreover, to avoid logical contradictions (inconsistencies) between different instances of an overridden operation, the user has to prove Liskov's principle for these situations: pre-conditions of the superclass must imply pre-conditions of the subclass, and post-conditions of a subclass must imply post-conditions of the superclass.

<footnote n="16">¹⁶In HOL, the Hilbert-Choice operator is a first-class element of the logical language.</footnote>
# 1. Formalization I: OCL Types and Core Definitions

**theory** UML-Types

**imports** Transcendental

**keywords** *Assert* :: *thy-decl*

and *Assert-local* :: *thy-decl*

**begin**

## 1.1. Preliminaries

### 1.1.1. Notations for the Option Type

First of all, we will use a more compact notation for the library option type which occur all over in our definitions and which will make the presentation more like a textbook:

**no-notation** ceiling (¬)

**no-notation** floor (⊥)

**type-notation** option (¬)⊥

**notation** Some (¬)

**notation** None (⊥)

These commands introduce an alternative, more compact notation for the type constructor (′α)⊥, namely (′α)⊥. Furthermore, the constructors X and ⊥ of the type (′α)⊥, namely X and ⊥.

The following function (corresponding to *the* in the Isabelle/HOL library) is defined as the inverse of the injection *Some*.

**fun** drop :: 'α option ⇒ 'α (¬)

**where** drop-lift[simp]: v = v

The definitions for the constants and operations based on functions will be geared towards a format that Isabelle can check to be a “conservative” (i. e., logically safe) axiomatic definition. By introducing an explicit interpretation function (which happens to be defined just as the identity since we are using a shallow embedding of OCL into HOL), all these definitions can be rewritten into the conventional semantic textbook format. To say it in other words: The interpretation function *Sem* as defined below is just a textual marker for presentation purposes, i. e. intended for readers used to conventional textbook notations on semantics. Since we use a “shallow embedding”, i. e. since we represent the syntax of OCL directly by HOL constants, the interpretation function is semantically not only superfluous, but from an Isabelle perspective strictly in the way for certain consistency checks performed by the definitional packages.

**definition** *Sem* :: 'a ⇒ 'a (I[·])

**where** I[x] = x

### 1.1.2. Common Infrastructure for all OCL Types

In order to have the possibility to nest collection types, such that we can give semantics to expressions like Set{Set{2}, null}, it is necessary to introduce a uniform interface for types having the invalid (= bottom) element. The reason is that we impose a data-invariant on raw-collection types_code which assures that the invalid element is not allowed inside the collection; all raw-collections of this form
were identified with the invalid element itself. The construction requires that the new collection type is not comparable with the raw-types (consisting of nested option type constructions), such that the data-invariant must be expressed in terms of the interface. In a second step, our base-types will be shown to be instances of this interface.

This uniform interface consists in a type class requiring the existence of a bot and a null element. The construction proceeds by abstracting the null (defined by `⊥` `⊥` on `'a option option'` to a null element, which may have an arbitrary semantic structure, and an undefinedness element `⊥` to an abstract undefinedness element `bot` (also written `⊥` whenever no confusion arises). As a consequence, it is necessary to redefine the notions of invalid, defined, valuation etc. on top of this interface.

This interface consists in two abstract type classes `bot` and `null` for the class of all types comprising a bot and a distinct null element.

```java
class bot =
    fixes bot :: 'a
    assumes nonEmpty : ∃ x. x ≠ bot
```

```java
class null = bot +
    fixes null :: 'a
    assumes null-is-valid : null ≠ bot
```

### 1.1.3. Accommodation of Basic Types to the Abstract Interface

In the following it is shown that the “option-option” type is in fact in the `null` class and that function spaces over these classes again “live” in these classes. This motivates the default construction of the semantic domain for the basic types (`Boolean`, `Integer`, `Real`, ...).

```
instantiation option :: (type)bot
begin
    definition bot-option-def: (bot::'a option) ≡ (None::'a option)
    instance ⟨proof⟩
end
```

```
instantiation option :: (bot)null
begin
    definition null-option-def: (null::'a::bot option) ≡ `bot`
    instance ⟨proof⟩
end
```

```
instantiation fun :: (type,bot) bot
begin
    definition bot-fun-def: bot ≡ (λ x. bot)
    instance ⟨proof⟩
end
```

```
instantiation fun :: (typenull) null
begin
    definition null-fun-def: (null::'a ⇒ 'b::null) ≡ (λ x. null)
    instance ⟨proof⟩
end
```

A trivial consequence of this adaption of the interface is that abstract and concrete versions of null are the same on base types (as could be expected).
### 1.1.4. The Common Infrastructure of Object Types (Class Types) and States.

Recall that OCL is a textual extension of the UML; in particular, we use OCL as means to annotate UML class models. Thus, OCL inherits a notion of *data* in the UML: UML class models provide classes, inheritance, types of objects, and subtypes connecting them along the inheritance hierarchy.

For the moment, we formalize the most common notions of objects, in particular the existence of object-identifiers (oid) for each object under which it can be referenced in a *state*.

type-synonym oid = nat

We refrained from the alternative:

type-synonym oid = ind

which is slightly more abstract but non-executable.

*States* in UML/OCL are a pair of

* a partial map from oid's to elements of an *object universe*, i.e. the set of all possible object representations.

* and an oid-indexed family of *associations*, i.e. finite relations between objects living in a state. These relations can be n-ary which we model by nested lists.

For the moment we do not have to describe the concrete structure of the object universe and denote it by the polymorphic variable `A`.

record ('A)state =
    heap :: oid → 'A
    assocs :: oid → ((oid list) list) list

In general, OCL operations are functions implicitly depending on a pair of pre- and post-state, i.e. *state transitions*. Since this will be reflected in our representation of OCL Types within HOL, we need to introduce the foundational concept of an object id (oid), which is just some infinite set, and some abstract notion of state.

type-synonym ('A)st = 'A state × 'A state

We will require for all objects that there is a function that projects the oid of an object in the state (we will settle the question how to define this function later). We will use the Isabelle type class mechanism [21] to capture this:

class object = fixes oid-of :: 'a ⇒ oid

Thus, if needed, we can constrain the object universe to objects by adding the following type class constraint:

typ 'A :: object

The major instance needed are instances constructed over options: once an object, options of objects are also objects.

instantiation option :: (object)object

begin

definition oid-of-option-def: oid-of x = oid-of (the x)

instance ⟨proof⟩

end

### 1.1.5. Common Infrastructure for all OCL Types (II): Valuations as OCL Types

Since OCL operations in general depend on pre- and post-states, we will represent OCL types as *functions* from pre- and post-state to some HOL raw-type that contains exactly the data in the OCL type — see below. This gives rise to the idea that we represent OCL types by *Valuations*.
Valuations are functions from a state pair (built upon data universe 'A) to an arbitrary null-type (i. e., containing at least a distinguished null and invalid element).

type-synonym ('A, 'α) val = 'A st ⇒ 'α::null

The definitions for the constants and operations based on valuations will be geared towards a format that Isabelle can check to be a "conservative" (i. e., logically safe) axiomatic definition. By introducing an explicit interpretation function (which happens to be defined just as the identity since we are using a shallow embedding of OCL into HOL), all these definitions can be rewritten into the conventional semantic textbook format as follows:

1.1.6. The fundamental constants 'invalid' and 'null' in all OCL Types

As a consequence of semantic domain definition, any OCL type will have the two semantic constants invalid (for exceptional, aborted computation) and null :

definition invalid ::= ('A, 'α::bot) val

where invalid ≡ λ τ. bot

This conservative Isabelle definition of the polymorphic constant invalid is equivalent with the text-
book definition:

lemma textbook-invalid: I[ invalid ] τ = bot
<proof>

Note that the definition :

definition null ::= "('A, 'α::null) val"

where "null ≡ λ τ. null"

is not necessary since we defined the entire function space over null types again as null-types; the
crucial definition is null ≡ λx. null . Thus, the polymorphic constant null is simply the result of a
general type class construction. Nevertheless, we can derive the semantic textbook definition for the
OCL null constant based on the abstract null:

lemma textbook-null-fun: I[null::('A, 'α::null) val] τ = (null::('α::null))
<proof>

1.2. Basic OCL Value Types

The structure of this section roughly follows the structure of Chapter 11 of the OCL standard [32],
which introduces the OCL Library.

The semantic domain of the (basic) boolean type is now defined as the Standard: the space of valuation
to ⟨⟨bool⟩⊥⟩⊥, i. e. the Boolean base type:

type-synonym Boolean<sub>base</sub> = bool option option

type-synonym ('A)Boolean = ('A,Boolean<sub>base</sub>) val

Because of the previous class definitions, Isabelle type-inference establishes that 'A Boolean lives
actually both in the type class UML-Types bot-class bot and null ; this type is sufficiently rich to contain
at least these two elements. Analogously we build:

type-synonym Integer<sub>base</sub> = int option option

type-synonym ('A)Integer = ('A, Integer<sub>base</sub>) val

type-synonym String<sub>base</sub> = string option option

type-synonym ('A)String = ('A, String<sub>base</sub>) val

type-synonym Real<sub>base</sub> = real option option

type-synonym ('A)Real = ('A, Real<sub>base</sub>) val
Since *Real* is again a basic type, we define its semantic domain as the valuations over *real option option* — i.e. the mathematical type of real numbers. The HOL-theory for *real* “Real” transcendental numbers such as $π$ and $e$ as well as infrastructure to reason over infinite convergent Cauchy-sequences (it is thus possible, in principle, to reason in Featherweight OCL that the sum of inverted two-s exponentials is actually 2.

If needed, a code-generator to compile *Real* to floating-point numbers can be added; this allows for mapping reals to an efficient machine representation; of course, this feature would be logically unsafe.

For technical reasons related to the Isabelle type inference for type-classes (we don't get the properties in the right order that class instantiation provides them, if we would follow the previous scheme), we give a slightly atypical definition:

```c
typedef Voidbase = {X::unit option option. X = bot ∨ X = null } <proof>
```

```c
type-synonym ('A) Void = ('A, Voidbase) val
```

## 1.3. Some OCL Collection Types

For the semantic construction of the collection types, we have two goals:

1. we want the types to be fully abstract, i. e., the type should not contain junk-elements that are not representable by OCL expressions, and

2. we want a possibility to nest collection types (so, we want the potential of talking about $Set(\text{Set}(\text{Sequences}(\text{Pairs}(X, Y)))))$.

The former principle rules out the option to define '$\alpha$ Set just by $(\mathfrak{A}, (\mathfrak{A} \text{ option option}) \text{ set}) \text{ val}$. This would allow sets to contain junk elements such as $\{\perp\}$ which we need to identify with undefinedness itself. Abandoning fully abstractness of rules would later on produce all sorts of problems when quantifying over the elements of a type. However, if we build an own type, then it must conform to our abstract interface in order to have nested types: arguments of type-constructors must conform to our abstract interface, and the result type too.

### 1.3.1. The Construction of the Pair Type (Tuples)

The core of an own type construction is done via a type definition which provides the base-type ('$\alpha$, '$\beta$) $Pair_{base}$. It is shown that this type “fits” indeed into the abstract type interface discussed in the previous section.

```c
typedef ('α, 'β) Pairbase = {X::('α::null × 'β::null) option option.
                                X = bot ∨ X = null ∨ (fst⊤X⊤ ≠ bot ∧ snd⊤X⊤ ≠ bot)}
<proof>
```

We “carve” out from the concrete type $\langle\langle'\alpha \times '\beta\rangle\rangle_{\perp}$ the new fully abstract type, which will not contain representations like $\ll_\perp(\perp, a)_{\perp}$ or $\ll_\perp(b, \perp)_{\perp}$. The type constructor $Pair\{x,y\}$ to be defined later will identify these with invalid.

instantiation $Pair_{base} :: (null, null)bot$

begin

definition bot-Pairbase-def: (bot-class bot :: ('a::null, 'b::null) Pairbase) ≡ Abs-Pairbase None

instance <proof>

end

instantiation $Pair_{base} :: (null, null)null$

begin

definition null-Pairbase-def: (null::('a::null, 'b::null) Pairbase) ≡ Abs-Pairbase None
instance $\langle proof \rangle$

end

... and lifting this type to the format of a valuation gives us:

**type-synonym** (`'A', 'α', 'β') `Pair` = (`'A'`, (`'α', 'β') `Pair`<sub>base</sub>) `val`

**type-notation** `Pair`<sub>base</sub> (`Pair`'(-,-')`)

### 1.3.2. The Construction of the Set Type

The core of an own type construction is done via a type definition which provides the raw-type '$α$ Set<sub>base</sub>. It is shown that this type “fits” indeed into the abstract type interface discussed in the previous section. Note that we make no restriction whatsoever to *finite* sets; while with the standards type-constructors only finite sets can be denoted, there is the possibility to define in fact infinite type constructors in Featherweight OCL (c.f. Section 2.9.1).

**typedef** '$α$ Set<sub>base</sub> = {$X::('α::null) \text{ set option option. } X = \text{bot} \lor X = \text{null} \lor (\forall x \in \Gamma X^\Gamma. x \neq \text{bot})$} $\langle proof \rangle$

**instantiation** Set<sub>base</sub> :: (null)bot

begin

**definition** `bot-Set<sub>base</sub>-def`: (`bot::('a::null) Set<sub>base</sub>`) $\equiv$ `Abs-Set<sub>base</sub> None`

instance $\langle proof \rangle$

end

**instantiation** Set<sub>base</sub> :: (null>null

begin

**definition** `null-Set<sub>base</sub>-def`: (`null::('a::null) Set<sub>base</sub>`) $\equiv$ `Abs-Set<sub>base</sub> None`

instance $\langle proof \rangle$

end

... and lifting this type to the format of a valuation gives us:

**type-synonym** (`'A', 'α`) Set = (`'A', 'α' Set<sub>base</sub>) `val`

**type-notation** `Set<sub>base</sub>` (`Set`'(-')`)

### 1.3.3. The Construction of the Bag Type

The core of an own type construction is done via a type definition which provides the raw-type '$α$ Bag<sub>base</sub> based on multi-sets from the HOL library. As in Sets, it is shown that this type “fits” indeed into the abstract type interface discussed in the previous section, and as in sets, we make no restriction whatsoever to *finite* multi-sets; while with the standards type-constructors only finite sets can be denoted, there is the possibility to define in fact infinite type constructors in Featherweight OCL (c.f. Section 2.9.1). However, while several null elements are possible in a Bag, there can't be no bottom (invalid) element in them.

**typedef** '$α$ Bag<sub>base</sub> = {$X::('α::null ⇒ nat) \text{ option option. } X = \text{bot} \lor X = \text{null} \lor \Gamma X^\Gamma \text{ bot} = 0$} $\langle proof \rangle$

**instantiation** Bag<sub>base</sub> :: (null)bot

begin

**definition** `bot-Bag<sub>base</sub>-def`: (`bot::('a::null) Bag<sub>base</sub>`) $\equiv$ `Abs-Bag<sub>base</sub> None`
instance `⟨proof⟩`

end

instantiation `Bag<base> :: (null)null`

begin

definition `null-Bag<base>-def: (null::('a::null) Bag<base>) ≡ Abs-Bag<base> ⊳ None]`

instance `⟨proof⟩`

end

... and lifting this type to the format of a valuation gives us:

type-synonym `(A, 'α) Bag = ('A, 'α Bag<base>) val`

type-notation `Bag<base> (Bag'(-))`

### 1.3.4. The Construction of the Sequence Type

The core of an own type construction is done via a type definition which provides the base-type '$α$ Sequence<sub>base</sub>. It is shown that this type “fits” indeed into the abstract type interface discussed in the previous section.

typedef '$α$ Sequence<base> = {X::('α::null) list option option.
    X = bot ∨ X = null ∨ (∀ x ∈ set ⌈X⌈. x ≠ bot)}
⟨proof⟩

instantiation `Sequence<base> :: (null)bot`

begin

definition `bot-Sequence<base>-def: (bot::('a::null) Sequence<base>) ≡ Abs-Sequence<base> None`

instance `⟨proof⟩`

end

instantiation `Sequence<base> :: (null)null`

begin

definition `null-Sequence<base>-def: (null::('a::null) Sequence<base>) ≡ Abs-Sequence<base> None]`

instance `⟨proof⟩`

end

... and lifting this type to the format of a valuation gives us:

type-synonym `(A, 'α) Sequence = ('A, 'α Sequence<base>) val`

type-notation `Sequence<base> (Sequence'(-))`

### 1.3.5. Discussion: The Representation of UML/OCL Types in Featherweight OCL

In the introduction, we mentioned that there is an “injective representation mapping” between the types of OCL and the types of Featherweight OCL (and its meta-language: HOL). This injectivity is at the heart of our representation technique — a so-called *shallow embedding* — and means: OCL types were mapped one-to-one to types in HOL, ruling out a representation where everything is mapped on some common HOL-type, say “OCL-expression”, in which we would have to sort out the typing of OCL and its impact on the semantic representation function in an own, quite heavy side-calculus.

After the previous sections, we are now able to exemplify this representation as follows:

We do not formalize the representation map here; however, its principles are quite straight-forward:
<table><caption>Table 1.1.: Correspondance between OCL types and HOL types</caption><thead><tr><th>OCL Type</th><th>HOL Type</th></tr></thead><tbody><tr><td>Boolean</td><td>'A Boolean</td></tr><tr><td>Boolean -> Boolean</td><td>'A Boolean ⇒ 'A Boolean</td></tr><tr><td>(Integer, Integer) -> Boolean</td><td>'A Integer ⇒ 'A Integer ⇒ 'A Boolean</td></tr><tr><td>Set Integer</td><td>('A, Integer<sub>base</sub>) Set</td></tr><tr><td>Set Integer -> Real</td><td>('A, Integer<sub>base</sub>) Set ⇒ 'A Real</td></tr><tr><td>Set Pair Integer, Boolean</td><td>('A, Pair Integer<sub>base</sub>, Boolean<sub>base</sub>) Set</td></tr><tr><td>Set &lt;T&gt;</td><td>('A, 'α) Set</td></tr></tbody></table>

1. cartesion products of arguments were curried,

2. constants of type T were mapped to valuations over the HOL-type for T,

3. functions $T \to T'$ were mapped to functions in HOL, where $T$ and $T'$ were mapped to the valuations for them, and

4. the arguments of type constructors `Set(T)` remain corresponding HOL base-types.

Note, furthermore, that our construction of “fully abstract types” (no junk, no confusion) assures that the logical equality to be defined in the next section works correctly and comes as element of the “lingua franca”, i. e. HOL.

`⟨ML⟩`

end
## 2. Formalization II: OCL Terms and Library Operations

theory UML-Logic

imports UML-Types

begin

### 2.1. The Operations of the Boolean Type and the OCL Logic

#### 2.1.1. Basic Constants

lemma bot-Boolean-def : (bot::('A)Boolean) = (λ τ. ⊥)
(proof)

lemma null-Boolean-def : (null::('A)Boolean) = (λ τ. ⊥_)
(proof)

definition true :: ('A)Boolean

where true = λ τ. ⊥_True_

definition false :: ('A)Boolean

where false = λ τ. ⊥_False_

lemma bool-split-0: X τ = invalid τ ∨ X τ = null τ ∨
X τ = true τ ∨ X τ = false τ

(proof)

lemma [simp]: false (a, b) = ⊥_False_

lemma [simp]: true (a, b) = ⊥_True_

lemma textbook-true: I[[true]] τ = ⊥_True_

lemma textbook-false: I[[false]] τ = ⊥_False_

#### 2.1.2. Validity and Definedness

However, this has also the consequence that core concepts like definedness, validity and even cp have to be redefined on this type class:

definition valid :: ('A,'a::null)val ⇒ ('A)Boolean (v - [100]100)

where v X = λ τ. if X τ = bot τ then false τ else true τ
<table><caption>Table 2.1.: Basic semantic constant definitions of the logic</caption><thead><tr><th>Name</th><th>Theorem</th></tr></thead><tbody><tr><td>textbook-invalid</td><td>I[invalid] τ = UML-Types bot-class bot</td></tr><tr><td>textbook-null-fun</td><td>I[null] τ = null</td></tr><tr><td>textbook-true</td><td>I[true] τ = True</td></tr><tr><td>textbook-false</td><td>I[false] τ = False</td></tr></tbody></table>

**lemma valid1[simp]:** $v$ invalid = false
<proof>

**lemma valid2[simp]:** $v$ null = true
<proof>

**lemma valid3[simp]:** $v$ true = true
<proof>

**lemma valid4[simp]:** $v$ false = true
<proof>

**lemma cp-valid:** $(v X) \tau = (v (\lambda . X \tau)) \tau$
<proof>

**definition defined:** $(\mathfrak{A}, a::null)\mathfrak{val} \Rightarrow (\mathfrak{A})\mathfrak{Boolean} (\delta - [100]100)$
**where** $\delta X \equiv \lambda \tau$. if $X \tau = \mathfrak{bot} \tau \lor X \tau = \mathfrak{null} \tau$ then false $\tau$ else true $\tau$

The generalized definitions of invalid and definedness have the same properties as the old ones :

**lemma defined1[simp]:** $\delta$ invalid = false
<proof>

**lemma defined2[simp]:** $\delta$ null = false
<proof>

**lemma defined3[simp]:** $\delta$ true = true
<proof>

**lemma defined4[simp]:** $\delta$ false = true
<proof>

**lemma defined5[simp]:** $\delta$ $\delta$ X = true
<proof>

**lemma defined6[simp]:** $\delta$ $v$ X = true
<proof>

**lemma valid5[simp]:** $v$ $v$ X = true
<proof>

**lemma valid6[simp]:** $v$ $\delta$ X = true
<proof>

**lemma cp-defined:** $(\delta X)\tau = (\delta (\lambda . X \tau)) \tau$
<proof>

The definitions above for the constants *defined* and *valid* can be rewritten into the conventional semantic "textbook" format as follows:

**lemma textbook-defined:** $I[\delta(X)] \tau = (\text{if } I[X] \tau = I[\mathfrak{bot}] \tau \lor I[X] \tau = I[\mathfrak{null}] \tau$
then $I[\mathfrak{false}] \tau$
else $I[\mathfrak{true}] \tau)$
<proof>

**lemma textbook-valid:** $I[v(X)] \tau = (\text{if } I[X] \tau = I[\mathfrak{bot}] \tau$
then $I[\mathfrak{false}] \tau$
else $I[\mathfrak{true}] \tau)$
<proof>

<caption>Table 2.2 and Table 2.3 summarize the results of this section.</caption>
<table><caption>Table 2.2.: Basic predicate definitions of the logic.</caption><thead><tr><th>Name</th><th>Theorem</th></tr></thead><tbody><tr><td>textbook-defined</td><td>I[[δ X]] τ = (if I[[X]] τ = I[[UML-Types bot-class bot]] τ ∨ I[[X]] τ = I[[null]] τ<br>then I[[false]] τ else I[[true]] τ)</td></tr><tr><td>textbook-valid</td><td>I[[υ X]] τ = (if I[[X]] τ = I[[UML-Types bot-class bot]] τ then I[[false]] τ else<br>I[[true]] τ)</td></tr></tbody></table>

<table><caption>Table 2.3.: Laws of the basic predicates of the logic.</caption><thead><tr><th>Name</th><th>Theorem</th></tr></thead><tbody><tr><td>defined1</td><td>δ invalid = false</td></tr><tr><td>defined2</td><td>δ null = false</td></tr><tr><td>defined3</td><td>δ true = true</td></tr><tr><td>defined4</td><td>δ false = true</td></tr><tr><td>defined5</td><td>δ δ X = true</td></tr><tr><td>defined6</td><td>δ υ X = true</td></tr></tbody></table>

### 2.1.3. The Equalities of OCL

The OCL contains a particular version of equality, written in Standard documents `=` and `<>` for its negation, which is referred as *weak referential equality* hereafter and for which we use the symbol `=` throughout the formal part of this document. Its semantics is motivated by the desire of fast execution, and similarity to languages like Java and C, but does not satisfy the needs of logical reasoning over OCL expressions and specifications. We therefore introduce a second equality, referred as *strong equality* or *logical equality* and written `≡` which is not present in the current standard but was discussed in prior texts on OCL like the Amsterdam Manifesto [18] and was identified as desirable extension of OCL in the Aachen Meeting [14] in the future 2.5 OCL Standard. The purpose of strong equality is to define and reason over OCL. It is therefore a natural task in Featherweight OCL to formally investigate the somewhat quite complex relationship between these two.

Strong equality has two motivations: a pragmatic one and a fundamental one.

1. The pragmatic reason is fairly simple: users of object-oriented languages want something like a "shallow object value equality". You will want to say a.boss ≜ b.boss@pre instead of

a.boss ≜ b.boss@pre **and** (* just the pointers are equal! *)

a.boss.name ≜ b.boss@pre.name@pre **and**

a.boss.age ≜ b.boss@pre.age@pre

Breaking a shallow-object equality down to referential equality of attributes is cumbersome, error-prone, and makes specifications difficult to extend (add for example an attribute sex to your class, and check in your OCL specification everywhere that you did it right with your simulation of strong equality). Therefore, languages like Java offer facilities to handle two different equalities, and it is problematic even in an execution oriented specification language to ignore shallow object equality because it is so common in the code.

2. The fundamental reason goes as follows: whatever you do to reason consistently over a language, you need the concept of equality: you need to know what expressions can be replaced by others because they *mean the same thing*. People call this also “Leibniz Equality” because this philosopher brought this principle first explicitly to paper and shed some light over it. It is the theoretic foundation of what you do in an optimizing compiler: you replace expressions by equal ones, which you hope are easier to evaluate. In a typed language, strong equality exists uniformly over all
types, it is “polymorphic” `=` `=` `:: α * α → bool`—this is the way that equality is defined in HOL itself. We can express Leibniz principle as one logical rule of surprising simplicity and beauty:

$$s = t \implies P(s) = P(t) \qquad (2.1)$$

“Whenever we know, that `s` is equal to `t`, we can replace the sub-expression `s` in a term `P` by `t` and we have that the replacement is equal to the original.”

While weak referential equality is defined to be strict in the OCL standard, we will define strong equality as non-strict. It is quite nasty (but not impossible) to define the logical equality in a strict way (the substitutivity rule above would look more complex), however, whenever references were used, strong equality is needed since references refer to particular states (pre or post), and that they mean the same thing can therefore not be taken for granted.

## Definition

The strict equality on basic types (actually on all types) must be exceptionally defined on `null`— otherwise the entire concept of null in the language does not make much sense. This is an important exception from the general rule that null arguments—especially if passed as “self”-argument—lead to invalid results.

We define strong equality extremely generic, even for types that contain a `null` or `⊥` element. Strong equality is simply polymorphic in Featherweight OCL, i. e., is defined identical for all types in OCL and HOL.

**definition** `StrongEq::[‘A st ⇒ ‘α,‘A st ⇒ ‘α] ⇒ (‘A)Boolean (infixl ≜ 30)`

**where** `X ≜ Y ≡ λ τ. ⊢X τ = Y τ ⊢`

From this follow already elementary properties like:

**lemma** `[simp,code-unfold]: (true ≜ false) = false`
`⟨proof⟩`

**lemma** `[simp,code-unfold]: (false ≜ true) = false`
`⟨proof⟩`

## Fundamental Predicates on Strong Equality

Equality reasoning in OCL is not humpty dumpty. While strong equality is clearly an equivalence:

**lemma** `StrongEq-refl [simp]: (X ≜ X) = true`
`⟨proof⟩`

**lemma** `StrongEq-sym`: `(X ≜ Y) = (Y ≜ X)`
`⟨proof⟩`

**lemma** `StrongEq-trans-strong [simp]`:

**assumes** `A`: `(X ≜ Y) = true`

**and** `B`: `(Y ≜ Z) = true`

**shows** `(X ≜ Z) = true`

`⟨proof⟩`

it is only in a limited sense a congruence, at least from the point of view of this semantic theory. The point is that it is only a congruence on OCL expressions, not arbitrary HOL expressions (with which we can mix Featherweight OCL expressions). A semantic—not syntactic—characterization of OCL expressions is that they are *context-passing* or *context-invariant*, i. e., the context of an entire OCL expression, i. e. the pre and post state it refers to, is passed constantly and unmodified to the sub-expressions, i. e., all sub-expressions inside an OCL expression refer to the same context. Expressed formally, this boils down to:
**lemma StrongEq-subst :**

assumes cp: $\bigwedge X. P(X)\tau = P(\lambda -. X \tau)\tau$

and eq: $(X \triangleq Y)\tau = true \ \tau$

shows $(P X \triangleq P Y)\tau = true \ \tau$

⟨proof⟩

**lemma defined7[simp]:** $\delta(X \triangleq Y) = true$

⟨proof⟩

**lemma valid7[simp]:** $v(X \triangleq Y) = true$

⟨proof⟩

**lemma cp-StrongEq:** $(X \triangleq Y) \tau = ((\lambda -. X \tau) \triangleq (\lambda -. Y \tau)) \tau$

⟨proof⟩

### 2.1.4. Logical Connectives and their Universal Properties

It is a design goal to give OCL a semantics that is as closely as possible to a “logical system” in a known sense; a specification logic where the logical connectives can not be understood other that having the truth-table aside when reading fails its purpose in our view.

Practically, this means that we want to give a definition to the core operations to be as close as possible to the lattice laws; this makes also powerful symbolic normalization of OCL specifications possible as a pre-requisite for automated theorem provers. For example, it is still possible to compute without any definedness and validity reasoning the DNF of an OCL specification; be it for test-case generations or for a smooth transition to a two-valued representation of the specification amenable to fast standard SMT-solvers, for example.

Thus, our representation of the OCL is merely a 4-valued Kleene-Logics with invalid as least, null as middle and true resp. false as unrelated top-elements.

**definition** *OclNot* :: ('A)Boolean $\Rightarrow$ ('A)Boolean (not)

where *not X* $\equiv$ $\lambda \tau . case X \tau$ of

$\bot$ $\Rightarrow$ $\bot$

| $\bot \perp$ | $\Rightarrow$ | $\bot \perp$ |

| $\bot$ $x$ | $\Rightarrow$ | $\bot$ $\neg$ $x$ |

**lemma cp-OclNot:** $(not X)\tau = (not (\lambda -. X \tau)) \tau$

⟨proof⟩

**lemma OclNot1[simp]:** *not invalid* = *invalid*

⟨proof⟩

**lemma OclNot2[simp]:** *not null* = *null*

⟨proof⟩

**lemma OclNot3[simp]:** *not true* = *false*

⟨proof⟩

**lemma OclNot4[simp]:** *not false* = *true*

⟨proof⟩

**lemma OclNot-not[simp]:** *not (not X)* = *X*

⟨proof⟩

**lemma OclNot-inject:** $\bigwedge x y. not x = not y \Rightarrow x = y$
**definition** OclAnd :: [('A)Boolean, ('A)Boolean] ⇒ ('A)Boolean (infixl and 30)

**where** X and Y ≡ (λ τ . case X τ of

<figure><img src="image_8.png" /></figure>

Note that *not* is not defined as a strict function; proximity to lattice laws implies that we *need* a definition of *not* that satisfies not(not(x))=x.

In textbook notation, the logical core constructs *not* and *op and* were represented as follows:

**lemma** textbook-OclNot:

<figure><img src="image_9.png" /></figure>

**lemma** textbook-OclAnd:

<figure><img src="image_10.png" /></figure>

**definition** OclOr :: [('A)Boolean, ('A)Boolean] ⇒ ('A)Boolean (infixl or 25)

**where** X or Y ≡ not(not X and not Y)

**definition** OclImplies :: [('A)Boolean, ('A)Boolean] ⇒ ('A)Boolean (infixl implies 25)

**where** X implies Y ≡ not X or Y

**lemma** cp-OclAnd: (X and Y) τ = ((λ -. X τ) and (λ -. Y τ)) τ

〈proof〉

**lemma** cp-OclOr: ((X::('A)Boolean) or Y) τ = ((λ -. X τ) or (λ -. Y τ)) τ

〈proof〉
lemma cp-OclImplies:(X implies Y) τ = ((λ -. X τ) implies (λ -. Y τ)) τ
<proof>

lemma OclAnd1[simp]: (invalid and true) = invalid
<proof>

lemma OclAnd2[simp]: (invalid and false) = false
<proof>

lemma OclAnd3[simp]: (invalid and null) = invalid
<proof>

lemma OclAnd4[simp]: (invalid and invalid) = invalid
<proof>

lemma OclAnd5[simp]: (null and true) = null
<proof>

lemma OclAnd6[simp]: (null and false) = false
<proof>

lemma OclAnd7[simp]: (null and null) = null
<proof>

lemma OclAnd8[simp]: (null and invalid) = invalid
<proof>

lemma OclAnd9[simp]: (false and true) = false
<proof>

lemma OclAnd10[simp]: (false and false) = false
<proof>

lemma OclAnd11[simp]: (false and null) = false
<proof>

lemma OclAnd12[simp]: (false and invalid) = false
<proof>

lemma OclAnd13[simp]: (true and true) = true
<proof>

lemma OclAnd14[simp]: (true and false) = false
<proof>

lemma OclAnd15[simp]: (true and null) = null
<proof>

lemma OclAnd16[simp]: (true and invalid) = invalid
<proof>

lemma OclAnd-idem[simp]: (X and X) = X
<proof>

lemma OclAnd-commute: (X and Y) = (Y and X)
<proof>

lemma OclAnd-false1[simp]: (false and X) = false
<proof>

lemma OclAnd-false2[simp]: (X and false) = false
<proof>

lemma OclAnd-true1[simp]: (true and X) = X
<proof>

lemma OclAnd-true2[simp]: (X and true) = X
〈proof〉

lemma OclAnd-bot1[simp]: $\bigwedge \tau. X \tau \neq \text{false } \tau \implies (\text{bot and } X) \tau = \text{bot } \tau$
〈proof〉

lemma OclAnd-bot2[simp]: $\bigwedge \tau. X \tau \neq \text{false } \tau \implies (X \text{ and bot } \tau) = \text{bot } \tau$
<proof>

lemma OclAnd-null1[simp]: $\bigwedge \tau. X \tau \neq \text{false } \tau \implies X \tau \neq \text{bot } \tau \implies (\text{null and } X) \tau = \text{null } \tau$
<proof>

lemma OclAnd-null2[simp]: $\bigwedge \tau. X \tau \neq \text{false } \tau \implies X \tau \neq \text{bot } \tau \implies (X \text{ and null } \tau) = \text{null } \tau$
<proof>

lemma OclAnd-assoc: $(X \text{ and } (Y \text{ and } Z)) = (X \text{ and } Y \text{ and } Z)$
<proof>

lemma OclOr1[simp]: $(\text{invalid or true}) = \text{true}$
<proof>

lemma OclOr2[simp]: $(\text{invalid or false}) = \text{invalid}$
<proof>

lemma OclOr3[simp]: $(\text{invalid or null}) = \text{invalid}$
<proof>

lemma OclOr4[simp]: $(\text{invalid or invalid}) = \text{invalid}$
<proof>

lemma OclOr5[simp]: $(\text{null or true}) = \text{true}$
<proof>

lemma OclOr6[simp]: $(\text{null or false}) = \text{null}$
<proof>

lemma OclOr7[simp]: $(\text{null or null}) = \text{null}$
<proof>

lemma OclOr8[simp]: $(\text{null or invalid}) = \text{invalid}$
<proof>

lemma OclOr-idem[simp]: $(X \text{ or } X) = X$
<proof>

lemma OclOr-commute: $(X \text{ or } Y) = (Y \text{ or } X)$
<proof>

lemma OclOr-false1[simp]: $(\text{false or } Y) = Y$
<proof>

lemma OclOr-false2[simp]: $(Y \text{ or false}) = Y$
<proof>

lemma OclOr-true1[simp]: $(\text{true or } Y) = \text{true}$
<proof>

lemma OclOr-true2: $(Y \text{ or true}) = \text{true}$
<proof>

lemma OclOr-bot1[simp]: $\bigwedge \tau. X \tau \neq \text{true } \tau \implies (\text{bot or } X) \tau = \text{bot } \tau$
<proof>
**lemma** *OclOr-bot2[simp]:* $\forall \tau. X \tau \neq \text{true} \tau \implies (X \text{ or } \text{bot}) \tau = \text{bot} \tau$
*(*proof*)*

**lemma** *OclOr-null1[simp]:* $\forall \tau. X \tau \neq \text{true} \tau \implies X \tau \neq \text{bot} \tau \implies (\text{null or } X) \tau = \text{null} \tau$
*(*proof*)*

**lemma** *OclOr-null2[simp]:* $\forall \tau. X \tau \neq \text{true} \tau \implies X \tau \neq \text{bot} \tau \implies (X \text{ or } \text{null}) \tau = \text{null} \tau$
*(*proof*)*

**lemma** *OclOr-assoc:* $(X \text{ or } (Y \text{ or } Z)) = (X \text{ or } Y \text{ or } Z)$
*(*proof*)*

**lemma** *deMorgan1:* $\text{not}(X \text{ and } Y) = ((\text{not } X) \text{ or } (\text{not } Y))$
*(*proof*)*

**lemma** *deMorgan2:* $\text{not}(X \text{ or } Y) = ((\text{not } X) \text{ and } (\text{not } Y))$
*(*proof*)*

**lemma** *OclImplies-true1[simp]:* $(\text{true implies } X) = X$
*(*proof*)*

**lemma** *OclImplies-true2[simp]:* $(X \text{ implies true}) = \text{true}$
*(*proof*)*

**lemma** *OclImplies-false1[simp]:* $(\text{false implies } X) = \text{true}$
*(*proof*)*

## 2.1.5. A Standard Logical Calculus for OCL

**definition** *OclValid* :: [('A)st, ('A)Boolean] $\Rightarrow$ bool ((1(-)/ $\models$ (-)) 50)

**where** $\tau \models P \equiv ((P \tau) = \text{true} \tau)$

**syntax** *OclNonValid* :: [('A)st, ('A)Boolean] $\Rightarrow$ bool ((1(-)/ $\models$ (-)) 50)

**translations** $\tau \not\models P == \neg(\tau \models P)$

### Global vs. Local Judgements

**lemma** *transform1:* $P = \text{true} \implies \tau \models P$
*(*proof*)*

**lemma** *transform1-rev:* $\forall \tau. \tau \models P \implies P = \text{true}$
*(*proof*)*

**lemma** *transform2:* $(P = Q) \implies ((\tau \models P) = (\tau \models Q))$
*(*proof*)*

**lemma** *transform2-rev:* $\forall \tau. (\tau \models \delta P) \land (\tau \models \delta Q) \land (\tau \models P) = (\tau \models Q) \implies P = Q$
*(*proof*)*

However, certain properties (like transitivity) can not be *transformed* from the global level to the local one, they have to be re-proven on the local level.

**lemma**

**assumes** $H: P = \text{true} \implies Q = \text{true}$

**shows** $\tau \models P \implies \tau \models Q$

*(*proof*)*
## Local Validity and Meta-logic

**lemma foundation1[simp]:** $\tau \models true$
*< proof >*

**lemma foundation2[simp]:** $\neg (\tau \models false)$
*< proof >*

**lemma foundation3[simp]:** $\neg (\tau \models invalid)$
*< proof >*

**lemma foundation4[simp]:** $\neg (\tau \models null)$
*< proof >*

**lemma bool-split[simp]:**
$(\tau \models (x \triangleq invalid)) \lor (\tau \models (x \triangleq null)) \lor (\tau \models (x \triangleq true)) \lor (\tau \models (x \triangleq false))$
*< proof >*

**lemma defined-split:**
$(\tau \models \delta x) = ((\neg(\tau \models (x \triangleq invalid))) \land (\neg(\tau \models (x \triangleq null))))$
*< proof >*

**lemma valid-bool-split:** $(\tau \models v A) = ((\tau \models A \triangleq null) \lor (\tau \models A) \lor (\tau \models not A))$
*< proof >*

**lemma defined-bool-split:** $(\tau \models \delta A) = ((\tau \models A) \lor (\tau \models not A))$
*< proof >*

**lemma foundation5:**
$\tau \models (P \text{ and } Q) \implies (\tau \models P) \land (\tau \models Q)$
*< proof >*

**lemma foundation6:**
$\tau \models P \implies \tau \models \delta P$
*< proof >*

**lemma foundation7[simp]:**
$(\tau \models not (\delta x)) = (\neg (\tau \models \delta x))$
*< proof >*

**lemma foundation7'[simp]:**
$(\tau \models not (v x)) = (\neg (\tau \models v x))$
*< proof >*

Key theorem for the $\delta$-closure: either an expression is defined, or it can be replaced (substituted via StrongEq-L-subst2; see below) by invalid or null. Strictness-reduction rules will usually reduce these substituted terms drastically.

**lemma foundation8:**
$(\tau \models \delta x) \lor (\tau \models (x \triangleq invalid)) \lor (\tau \models (x \triangleq null))$
*< proof >*

**lemma foundation9:**
$\tau \models \delta x \implies (\tau \models not x) = (\neg (\tau \models x))$
〈proof〉

**lemma foundation9':**

$\tau \models \text{not } x \implies \neg (\tau \models x)$

〈proof〉

**lemma foundation9'':**

$\tau \models \text{not } x \implies \tau \models \delta x$

〈proof〉

**lemma foundation10:**

$\tau \models \delta x \implies \tau \models \delta y \implies (\tau \models (x \text{ and } y)) = ((\tau \models x) \land (\tau \models y))$

〈proof〉

**lemma foundation10':** $(\tau \models (A \text{ and } B)) = ((\tau \models A) \land (\tau \models B))$

〈proof〉

**lemma foundation11:**

$\tau \models \delta x \implies \tau \models \delta y \implies (\tau \models (x \text{ or } y)) = ((\tau \models x) \lor (\tau \models y))$

〈proof〉

**lemma foundation12:**

$\tau \models \delta x \implies (\tau \models (x \text{ implies } y)) = ((\tau \models x) \rightarrow (\tau \models y))$

〈proof〉

**lemma foundation13:** $(\tau \models A \triangleq \text{true}) = (\tau \models A)$

〈proof〉

**lemma foundation14:** $(\tau \models A \triangleq \text{false}) = (\tau \models \text{not } A)$

〈proof〉

**lemma foundation15:** $(\tau \models A \triangleq \text{invalid}) = (\tau \models \text{not}(\upsilon A))$

〈proof〉

**lemma foundation16:** $\tau \models (\delta X) = (X \tau \neq \text{bot} \land X \tau \neq \text{null})$

〈proof〉

**lemma foundation16'**: $\neg (\tau \models (\delta X)) = ((\tau \models (X \triangleq \text{invalid})) \lor (\tau \models (X \triangleq \text{null})))$

〈proof〉

**lemma foundation16'**: $(\tau \models (\delta X)) = (X \tau \neq \text{invalid} \land X \tau \neq \text{null} \tau)$

〈proof〉

**lemma foundation18:** $(\tau \models (\upsilon X)) = (X \tau \neq \text{invalid} \tau)$

〈proof〉

**lemma foundation18'**: $(\tau \models (\upsilon X)) = (X \tau \neq \text{bot})$

〈proof〉
**lemma foundation18''**: $(\tau \models (\nu X)) = (\neg(\tau \models (X \triangleq \text{invalid})))$
*<proof>*

**lemma foundation20**: $\tau \models (\delta X) \implies \tau \models \nu X$
*<proof>*

**lemma foundation21**: $(\text{not } A \triangleq \text{ not } B) = (A \triangleq B)$
*<proof>*

**lemma foundation22**: $(\tau \models (X \triangleq Y)) = (X \tau = Y \tau)$
*<proof>*

**lemma foundation23**: $(\tau \models P) = (\tau \models (\lambda . P \tau))$
*<proof>*

**lemma foundation24**: $(\tau \models \text{not}(X \triangleq Y)) = (X \tau \neq Y \tau)$
*<proof>*

**lemma foundation25**: $\tau \models P \implies \tau \models (P \text{ or } Q)$
*<proof>*

**lemma foundation25'**: $\tau \models Q \implies \tau \models (P \text{ or } Q)$
*<proof>*

**lemma foundation26**:

assumes $\text{defP}: \tau \models \delta P$

assumes $\text{defQ}: \tau \models \delta Q$

assumes $H: \tau \models (P \text{ or } Q)$

assumes $P: \tau \models P \implies R$

assumes $Q: \tau \models Q \implies R$

shows $R$

*<proof>*

**lemma foundation27**: $\tau \models A \implies (\tau \models A \text{ implies } B) = (\tau \models B)$
*<proof>*

**lemma defined-not-I**: $\tau \models \delta (x) \implies \tau \models \delta (\text{not } x)$
*<proof>*

**lemma valid-not-I**: $\tau \models \nu (x) \implies \tau \models \nu (\text{not } x)$
*<proof>*

**lemma defined-and-I**: $\tau \models \delta (x) \implies \tau \models \delta (y) \implies \tau \models \delta (x \text{ and } y)$
*<proof>*

**lemma valid-and-I**: $\tau \models \nu (x) \implies \tau \models \nu (y) \implies \tau \models \nu (x \text{ and } y)$
*<proof>*

**lemma defined-or-I**: $\tau \models \delta (x) \implies \tau \models \delta (y) \implies \tau \models \delta (x \text{ or } y)$
*<proof>*

**lemma valid-or-I**: $\tau \models \nu (x) \implies \tau \models \nu (y) \implies \tau \models \nu (x \text{ or } y)$
*<proof>*
## Local Judgements and Strong Equality

**lemma** *StrongEq-L-refl*: $\tau \models (x \triangleq x)$
*(*proof*)

**lemma** *StrongEq-L-sym*: $\tau \models (x \triangleq y) \implies \tau \models (y \triangleq x)$
*(*proof*)

**lemma** *StrongEq-L-trans*: $\tau \models (x \triangleq y) \implies \tau \models (y \triangleq z) \implies \tau \models (x \triangleq z)$
*(*proof*)

In order to establish substitutivity (which does not hold in general HOL formulas) we introduce the following predicate that allows for a calculus of the necessary side-conditions.

**definition** *cp*: $((\mathfrak{A}, \alpha) \text{ val} \Rightarrow (\mathfrak{A}, \beta) \text{ val}) \Rightarrow \mathbf{bool}$

**where** $cp P \equiv (\exists f. \forall X \tau. P X \tau = f (X \tau) \tau)$

The rule of substitutivity in Featherweight OCL holds only for context-passing expressions, i. e. those that pass the context $\tau$ without changing it. Fortunately, all operators of the OCL language satisfy this property (but not all HOL operators).

**lemma** *StrongEq-L-subst1*: $\bigwedge \tau. cp P \implies \tau \models (x \triangleq y) \implies \tau \models (P x \triangleq P y)$
*(*proof*)

**lemma** *StrongEq-L-subst2*: $\bigwedge \tau. cp P \implies \tau \models (x \triangleq y) \implies \tau \models (P x) \implies \tau \models (P y)$
*(*proof*)

**lemma** *StrongEq-L-subst2-rev*: $\tau \models y \triangleq x \implies cp P \implies \tau \models P x \implies \tau \models P y$
*(*proof*)

**lemma** *StrongEq-L-subst3*: $\text{assumes } cp: cp P$
$\text{and } \text{eq: } \tau \models (x \triangleq y)$
$\text{shows } (\tau \models P x) = (\tau \models P y)$
*(*proof*)

**lemma** *StrongEq-L-subst3-rev*: $\text{assumes } eq: \tau \models (x \triangleq y)$
$\text{and } cp: cp P$
$\text{shows } (\tau \models P x) = (\tau \models P y)$
*(*proof*)

**lemma** *StrongEq-L-subst4-rev*: $\text{assumes } eq: \tau \models (x \triangleq y)$
$\text{and } cp: cp P$
$\text{shows } (\neg(\tau \models P x)) = (\neg(\tau \models P y))$
$\text{thm } \text{arg-cong}[\text{of - - Not}]$
*(*proof*)

**lemma** *cpI1*: $(\forall X \tau. f X \tau = f(\lambda-. X \tau) \tau) \implies cp P \implies cp(\lambda X. f (P X))$
*(*proof*)

**lemma** *cpI2*: $(\forall X Y \tau. f X Y \tau = f(\lambda-. X \tau)(\lambda-. Y \tau) \tau) \implies$
$cp P \implies cp Q \implies cp(\lambda X. f (P X) (Q X))$
*(*proof*)
**lemma cpI3:**

$$ (\forall X Y Z \tau. f X Y Z \tau = f(\lambda-. X \tau)(\lambda-. Y \tau)(\lambda-. Z \tau) \tau) \implies \\ cp P \implies cp Q \implies cp R \implies cp(\lambda X. f (P X) (Q X) (R X)) \\ \langle proof \rangle $$

**lemma cpI4:**

$$ (\forall W X Y Z \tau. f W X Y Z \tau = f(\lambda-. W \tau)(\lambda-. X \tau)(\lambda-. Y \tau)(\lambda-. Z \tau) \tau) \implies \\ cp P \implies cp Q \implies cp R \implies cp S \implies cp(\lambda X. f (P X) (Q X) (R X) (S X)) \\ \langle proof \rangle $$

**lemma cpI5:**

$$ (\forall V W X Y Z \tau. f V W X Y Z \tau = f(\lambda-. V \tau)(\lambda-. W \tau)(\lambda-. X \tau)(\lambda-. Y \tau)(\lambda-. Z \tau) \tau) \implies \\ cp N \implies cp P \implies cp Q \implies cp R \implies cp S \implies cp(\lambda X. f (N X) (P X) (Q X) (R X) (S X)) \\ \langle proof \rangle $$

**lemma cp-const : cp(\lambda-. c)**

$$ \langle proof \rangle $$

**lemma cp-id : cp(\lambda X. X)**

$$ \langle proof \rangle \textbf{lemmas} cp-intro[into!, simp, code-unfold] = \\ cp-const \\ cp-id \\ cp-defined[THEN allI[THEN allI[THEN cpI1], of defined]] \\ cp-valid[THEN allU[THEN allU[THEN cpI1], of valid]] \\ cp-OclNot[THEN allI[THEN allI[THEN cpI1], of not]] \\ cp-OclAnd[THEN allI[THEN allI[THEN allI[THEN cpI2]], of op and]] \\ cp-OclOr[THEN allI[THEN allI[THEN allI[THEN cpI2]], of op or]] \\ cp-OclImplies[THEN allI[THEN allI[THEN allI[THEN cpI2]], of op implies]] \\ cp-StrongEq[THEN allI[THEN allI[THEN allI[THEN cpI2]], \\ \qquad of StrongEq]] $$

### 2.1.6. OCL's if then else endif

**definition OclIf** :: [(‘A’)Boolean , (‘A’,‘α::null) val , (‘A’,‘α) val] ⇒ (‘A’,‘α) val
(if (-) then (-) else (-) endif [10,10,10]50)

**where** (if C then B₁ else B₂ endif) = (λ τ. if (δ C) τ = true τ
then (if (C τ) = true τ
then B₁ τ
else B₂ τ)
else invalid τ)

**lemma cp-OclIf:**((if C then B₁ else B₂ endif) τ =
(if (λ -. C τ) then (λ -. B₁ τ) else (λ -. B₂ τ) endif) τ)

$$ \langle proof \rangle \textbf{lemmas} cp-intro[into!, simp, code-unfold] = \\ cp-intro \\ cp-OclIf[THEN allI[THEN allI[THEN allI[THEN cpI3]], of OclIf]]\textbf{lemma OclIf-invalid} \\ [simp]: (if invalid then B₁ else B₂ endif) = invalid \\ \langle proof \rangle $$

**lemma OclIf-null [simp]:** (if null then B₁ else B₂ endif) = invalid
$\langle proof \rangle$

**lemma OclIf-true [simp]:** (if true then B₁ else B₂ endif) = B₁
$\langle proof \rangle$
**lemma** *OclIf-true'* [simp]: $\tau \models P \implies (\mathit{if} P \mathit{then} B_1 \mathit{else} B_2 \mathit{endif})\tau = B_1 \tau$
<code>(proof)</code>

**lemma** *OclIf-true''* [simp]: $\tau \models P \implies \tau \models (\mathit{if} P \mathit{then} B_1 \mathit{else} B_2 \mathit{endif}) \triangleq B_1$
<code>(proof)</code>

**lemma** *OclIf-false* [simp]: (if false then $B_1$ else $B_2$endif) = $B_2$
<code>(proof)</code>

**lemma** *OclIf-false'* [simp]: $\tau \models \mathit{not} P \implies (\mathit{if} P \mathit{then} B_1 \mathit{else} B_2 \mathit{endif})\tau = B_2 \tau$
<code>(proof)</code>

**lemma** *OclIf-idem1* [simp]: (if $\delta X$ then $A$ else $A$endif) = $A$
<code>(proof)</code>

**lemma** *OclIf-idem2* [simp]: (if $\nu X$ then $A$ else $A$endif) = $A$
<code>(proof)</code>

**lemma** *OclNot-if* [simp]:
$\mathit{not}(\mathit{if} P \mathit{then} C \mathit{else} E \mathit{endif}) = (\mathit{if} P \mathit{then} \mathit{not} C \mathit{else} \mathit{not} E \mathit{endif})$
<code>(proof)</code>

### 2.1.7. Fundamental Predicates on Basic Types: Strict (Referential) Equality

In contrast to logical equality, the OCL standard defines an equality operation which we call “strict referential equality”. It behaves differently for all types—on value types, it is basically a strict version of strong equality, for defined values it behaves identical. But on object types it will compare their references within the store. We introduce strict referential equality as an *overloaded* concept and will handle it for each type instance individually.

**consts** *StrictRefEq* :: [(‘A’,‘a’)val, (‘A’,‘a’)val] ⇒ (‘A’)Boolean (*infixl* `:=` 30)

with term "not" we can express the notation:

**syntax**

notequal :: ('A')Boolean ⇒ ('A')Boolean ⇒ ('A')Boolean (*infix* <> 40)

**translations**

$a <> b == CONST OclNot(a := b)$

We will define instances of this equality in a case-by-case basis.

### 2.1.8. Laws to Establish Definedness (δ-closure)

For the logical connectives, we have — beyond $\tau \models P \implies \tau \models \delta P$ — the following facts:

**lemma** *OclNot-defargs*:
$\tau \models (\mathit{not} P) \implies \tau \models \delta P$
<code>(proof)</code>

**lemma** *OclNot-contrapos-nn*:
assumes $A: \tau \models \delta A$
assumes $B: \tau \models \mathit{not} B$
assumes $C: \tau \models A \implies \tau \models B$
shows $\tau \models \mathit{not} A$
<code>(proof)</code>
### 2.1.9. A Side-calculus for Constant Terms

**definition** `const X ≡ ∀ τ τ'. X τ = X τ'`

**lemma** `const-charn: const X = X τ = X τ'`
*(*proof*)*

**lemma** `const-subst:`

assumes `const-X: const X`

and `const-Y: const Y`

and `eq: X τ = Y τ`

and `cp-P: cp P`

and `pp: P Y τ = P Y τ'`

shows `P X τ = P X τ'`

*(*proof*)*

**lemma** `const-imply2:`

assumes `∠τ τ'. P τ = P τ' = ⇒ Q τ = Q τ'`

shows `const P = ⇒ const Q`

*(*proof*)*

**lemma** `const-imply3:`

assumes `∠τ τ'. P τ = P τ' = ⇒ Q τ = Q τ' = ⇒ R τ = R τ'`

shows `const P = ⇒ const Q = ⇒ const R`

*(*proof*)*

**lemma** `const-imply4:`

assumes `∠τ τ'. P τ = P τ' = ⇒ Q τ = Q τ' = ⇒ R τ = R τ' = ⇒ S τ = S τ'`

shows `const P = ⇒ const Q = ⇒ const R = ⇒ const S`

*(*proof*)*

**lemma** `const-lam`: `const (λ-. e)`

*(*proof*)*

**lemma** `const-true[simp]`: `const true`

*(*proof*)*

**lemma** `const-false[simp]`: `const false`

*(*proof*)*

**lemma** `const-null[simp]`: `const null`

*(*proof*)*

**lemma** `const-invalid [simp]`: `const invalid`

*(*proof*)*

**lemma** `const-bot[simp]`: `const bot`

*(*proof*)*

**lemma** `const-defined`:

assumes `const X`

shows `const (δ X)`

*(*proof*)*
**lemma const-valid :**
assumes const X
shows const (v X)
<proof>

**lemma const-OclAnd :**
assumes const X
assumes const X'
shows const (X and X')
<proof>

**lemma const-OclNot :**
assumes const X
shows const (not X)
<proof>

**lemma const-OclOr :**
assumes const X
assumes const X'
shows const (X or X')
<proof>

**lemma const-OclImplies :**
assumes const X
assumes const X'
shows const (X implies X')
<proof>

**lemma const-StrongEq:**
assumes const X
assumes const X'
shows const(X ≜ X')
<proof>

**lemma const-OclIf :**
assumes const B
and const C1
and const C2
shows const (if B then C1 else C2 endif)
<proof>

**lemma const-OclValid1:**
assumes const x
shows (τ |= δ x) = (τ' |= δ x)
<proof>

**lemma const-OclValid2:**
assumes const x
shows (τ |= v x) = (τ' |= v x)
<proof>
lemma const-HOL-if : const C = ⇒ const D = ⇒ const F = ⇒ const (λτ. if C τ then D τ else F τ)
<proof>

lemma const-HOL-and: const C = ⇒ const D = ⇒ const (λτ. C τ ∧ D τ)
<proof>

lemma const-HOL-eq : const C = ⇒ const D = ⇒ const (λτ. C τ = D τ)
<proof>

lemmas const-ss = const-bot const-null const-invalid const-false const-true const-lam
const-defined const-valid const-StrongEq const-OclNot const-OclAnd
const-OclOr const-OclImplies const-OclIf
const-HOL-if const-HOL-and const-HOL-eq

Miscellaneous: Overloading the syntax of “bottom”

notation bot (⊥)

end

theory UML-PropertyProfiles

imports UML-Logic

begin

## 2.2. Property Profiles for OCL Operators via Isabelle Locales

We use the Isabelle mechanism of a *Locale* to generate the common lemmas for each type and operator; Locales can be seen as a functor that takes a local theory and generates a number of theorems. In our case, we will instantiate later these locales by the local theory of an operator definition and obtain the common rules for strictness, definedness propagation, context-passingness and constance in a systematic way.

### 2.2.1. Property Profiles for Monadic Operators

locale profile-mono-scheme-defined =

fixes f :: ('A, 'α::null) val ⇒ ('A, 'β::null) val

fixes g

assumes def-scheme : (f x) ≡ λ τ. if (δ x) τ = true τ then g (x τ) else invalid τ

begin

lemma strict[simp, code-unfold]: f invalid = invalid

<proof>

lemma null-strict[simp, code-unfold]: f null = invalid

<proof>

lemma cp0 : f X τ = f (λ -. X τ) τ

<proof>

lemma cp[simp, code-unfold] : cp P = ⇒ cp (λX. f (P X))

<proof>

end
locale profile-mono-schemeV =

fixes f :: ('A,'α::null)val ⇒ ('A,'β::null)val

fixes g

assumes def-scheme: (f x) ≡ λ τ. if (υ x) τ = true τ then g (x τ) else invalid τ

begin

lemma strict[simp,code-unfold]: f invalid = invalid
<proof>

lemma cp0 : f X τ = f (λ -. X τ) τ
<proof>

lemma cp[simp,code-unfold] : cp P = ⇒ cp (λX. f (P X))
<proof>

end

locale profile-mono<sub>d</sub> = profile-mono-scheme-defined +

assumes A x. x ≠ bot = ⇒ x ≠ null = ⇒ g x ≠ bot
begin

lemma const[simp,code-unfold] :
  assumes C1 : const X
  shows const(f X)
  <proof>

end

locale profile-mono0 = profile-mono-scheme-defined +

assumes def-body: A x. x ≠ bot = ⇒ x ≠ null = ⇒ g x ≠ bot ∧ g x ≠ null

sublocale profile-mono0 < profile-mono<sub>d</sub>
<proof>

context profile-mono0

begin

lemma def-homo[simp,code-unfold]: δ(f x) = (δ x)
<proof>

lemma def-valid-then-def: υ(f x) = (δ(f x))
<proof>

end

### 2.2.2. Property Profiles for Single

locale profile-single =

fixes d:: ('A, 'a::null)val ⇒ 'A Boolean

assumes d-strict[simp,code-unfold]: d invalid = false

assumes d-cp0: d X τ = d (λ -. X τ) τ

assumes d-const[simp,code-unfold]: const X = ⇒ const (d X)

### 2.2.3. Property Profiles for Binary Operators

definition bin' f g d<sub>x</sub> d<sub>y</sub> X Y =

$$
\begin{align*}
(f X Y = (\lambda \tau. \text{if } (d_x X) \tau = \text{true } \tau \land (d_y Y) \tau = \text{true } \tau \\
\qquad \text{then } g X Y \tau \\
\qquad \text{else invalid } \tau))
\end{align*}
$$

definition bin' f g = bin' f (λX Y τ. g (X τ) (Y τ))
lemmas [simp, code-unfold] = bin'-def bin-def

locale profile-bin-scheme =

fixes $d_x :: ('\A, 'a::null) val \Rightarrow '\A Boolean$

fixes $d_y :: ('\A, 'b::null) val \Rightarrow '\A Boolean$

fixes $f :: ('\A, 'a::null) val \Rightarrow ('\A, 'b::null) val \Rightarrow ('\A, 'c::null) val$

fixes $g$

assumes $d_x' : profile-single d_x$

assumes $d_y' : profile-single d_y$

assumes $d_x - d_y$-homo[simp, code-unfold]: $cp (f X) \Rightarrow$

$$ cp (\lambda x. f x Y) \Rightarrow $$

$$ f X \text{ invalid} = \text{invalid} \Rightarrow $$

$$ f \text{ invalid } Y = \text{invalid} \Rightarrow $$

$$ (\neg (\tau \models d_x X) \lor \neg (\tau \models d_y Y)) \Rightarrow $$

$$ \tau \models (\delta f X Y \triangleq (d_x X \text{ and } d_y Y)) $$

assumes def-scheme''[simplified]: bin f g $d_x$ $d_y$ X Y

assumes $1: \tau \models d_x X \Rightarrow \tau \models d_y Y \Rightarrow \tau \models \delta f X Y$

begin

interpretation $d_x$: profile-single $d_x$ $\langle$proof$\rangle$

interpretation $d_y$: profile-single $d_y$ $\langle$proof$\rangle$

lemma strict1[simp, code-unfold] : $f \text{ invalid } y = \text{ invalid} \langle proof \rangle$

lemma strict2[simp, code-unfold] : $f x \text{ invalid} = \text{ invalid} \langle proof \rangle$

lemma $cp0: f X Y \tau = f (\lambda -. X \tau) (\lambda -. Y \tau) \tau$ 	$\langle proof \rangle$

lemma $cp[simp, code-unfold]$: $cp P \implies cp Q \implies cp (\lambda X. f (P X) (Q X)) \langle proof \rangle$

lemma def-homo[simp, code-unfold]: $\delta(f x y) = (d_x x \text{ and } d_y y) \langle proof \rangle$

lemma def-valid-then-def: $v(f x y) = (\delta(f x y)) \langle proof \rangle$

lemma defined-args-valid: $(\tau \models \delta(f x y)) = ((\tau \models d_x x) \land (\tau \models d_y y)) \langle proof \rangle$

lemma const[simp, code-unfold] :

assumes $C1 : \text{const } X \text{ and } C2 : \text{const } Y$

shows $\text{const}(f X Y)$

$\langle proof \rangle$

end

In our context, we will use Locales as “Property Profiles” for OCL operators; if an operator *f* is of profile *profile-bin-scheme defined f g* we know that it satisfies a number of properties like *strict1* or *strict2* i. e. *f invalid y = invalid* and *f null y = invalid*. Since some of the more advanced Locales come with 10 - 15 theorems, property profiles represent a major structuring mechanism for the OCL library.

locale profile-bin-scheme-defined =

fixes $d_y :: ('\A, 'b::null) val \Rightarrow '\A Boolean$

fixes $f :: ('\A, 'a::null) val \Rightarrow ('\A, 'b::null) val \Rightarrow ('\A, 'c::null) val$

fixes $g$
assumes $d_y$: profile-single $d_y$

assumes $d_y$-homo[simp, code-unfold]: cp (f X) $\Rightarrow$ 
$f X \text{ invalid} \quad \text{invalid} \quad \Rightarrow$
$\neg \tau \models d_y Y \quad \Rightarrow$
$\tau \models \delta f X Y \quad \triangleq \quad (\delta X \text{ and } d_y Y)$

assumes def-scheme'[simplified]: bin f g defined $d_y$ X Y

assumes def-body': $\bigwedge x y \tau$. $x \neq \text{bot} \implies x \neq \text{null} \implies (d_y y) \tau = \text{true} \tau \implies g x (y \tau) \neq \text{bot} \land g x (y \tau) \neq \text{null}$

begin

lemma strict3[simp, code-unfold]: f null y = invalid
(proof)

end

sublocale profile-bin-scheme-defined < profile-bin-scheme defined
(proof)

locale profile-bin$_{d-d}$ =

fixes f::('A,'a::null)val ⇒ ('A,'b::null)val ⇒ ('A,'c::null)val

fixes g

assumes def-scheme[simplified]: bin f g defined defined X Y

assumes def-body: $\bigwedge x y$. $x \neq \text{bot} \implies x \neq \text{null} \implies y \neq \text{bot} \implies y \neq \text{null} \implies g x y \neq \text{bot} \land g x y \neq \text{null}$

begin

lemma strict4[simp, code-unfold]: f x null = invalid
(proof)

end

sublocale profile-bin$_{d-d}$ < profile-bin-scheme-defined defined
(proof)

locale profile-bin$_{d-v}$ =

fixes f::('A,'a::null)val ⇒ ('A,'b::null)val ⇒ ('A,'c::null)val

fixes g

assumes def-scheme[simplified]: bin f g defined valid X Y

assumes def-body: $\bigwedge x y$. $x \neq \text{bot} \implies x \neq \text{null} \implies y \neq \text{bot} \implies g x y \neq \text{bot} \land g x y \neq \text{null}$

sublocale profile-bin$_{d-v}$ < profile-bin-scheme-defined valid
(proof)

locale profile-bin$_{StrongEq-v-v}$ =

fixes f :: ('A,'a::null) val ⇒ ('A,'a::null) val ⇒ ('A) Boolean

assumes def-scheme[simplified]: bin' f StrongEq valid valid X Y

sublocale profile-bin$_{StrongEq-v-v}$ < profile-bin-scheme valid valid f $\lambda x$ y. $\sqsubseteq x = y \sqsubseteq$ 
(proof)

context profile-bin$_{StrongEq-v-v}$

begin

lemma idem[simp, code-unfold]: f null null = true
(proof)

lemma defargs: $\tau \models f x y \implies (\tau \models v x) \land (\tau \models v y)$
(proof)

lemma defined-args-valid' : $\delta (f x y) = (v x \text{ and } v y)$
(proof)
lemma refl-ext[simp,code-unfold] : (f x x) = (if (v x) then true else invalid end if)
(proof)

lemma sym : τ ⊨ (f x y) ⇒ τ ⊨ (f y x)
(proof)

lemma symmetric : (f x y) = (f y x)
(proof)

lemma trans : τ ⊨ (f x y) ⇒ τ ⊨ (f y z) ⇒ τ ⊨ (f x z)
(proof)

lemma StrictRefEq-vs-StrongEq: τ ⊨(υ x) ⇒ τ ⊨(υ y) ⇒ (τ ⊨((f x y) ≜ (x ≜ y)))
(proof)

end

locale profile-bin_v_v =

fixes f :: ('A, 'α::null) val ⇒ ('A, 'β::null) val ⇒ ('A, 'γ::null) val

fixes g

assumes def-scheme[simplified]: bin f g valid valid X Y

assumes def-body: ¬ x y. x ≠ bot ⇒ y ≠ bot ⇒ g x y ≠ bot ∧ g x y ≠ null

sublocale profile-bin_v_v < profile-bin-scheme valid valid
(proof)

end

theory UML-Boolean

imports ../UML-PropertyProfiles

begin

### 2.2.4. Fundamental Predicates on Basic Types: Strict (Referential) Equality

Here is a first instance of a definition of strict value equality—for the special case of the type 'A Boolean, it is just the strict extension of the logical equality:

defs (overloaded) StrictRefEq[$\mathbb{Q}_{\text{Boolean}}$][code-unfold] :

(x::('A)Boolean) . = y = λ τ. if (v x) τ = true τ ∧ (v y) τ = true τ
then (x = y)τ
else invalid τ

which implies elementary properties like:

lemma [simp,code-unfold] : (true = false) = false
(proof)

lemma [simp,code-unfold] : (false = true) = false
(proof)

lemma null-non-false [simp,code-unfold]: (null = false) = false
(proof)

lemma null-non-true [simp,code-unfold]: (null = true) = false
(proof)
**lemma** `false-non-null [simp,code-unfold]: (false . = null) = false`
`⟨proof⟩`

**lemma** `true-non-null [simp,code-unfold]: (true . = null) = false`
`⟨proof⟩`

With respect to strictness properties and miscelleanous side-calculi, strict referential equality behaves on booleans as described in the *profile-bin<sub>StrongEq<sup>-v</sup>-v</sub>*:

**interpretation** `StrictRefEqBoolean`: `profile-bin<sub>StrongEq<sup>-v</sup>-v</sub> λ x y. (x::('A)Boolean) . = y`
`⟨proof⟩`

In particular, it is strict, cp-preserving and const-preserving. In particular, it generates the simplifier rules for terms like:

**lemma** `(invalid . = false) = invalid ⟨proof⟩`

**lemma** `(invalid . = true) = invalid ⟨proof⟩`

**lemma** `(false . = invalid) = invalid ⟨proof⟩`

**lemma** `(true . = invalid) = invalid ⟨proof⟩`

**lemma** `((invalid::('A)Boolean) . = invalid) = invalid ⟨proof⟩`

Thus, the weak equality is *not* reflexive.

### 2.2.5. Test Statements on Boolean Operations.

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to *True*.

Elementary computations on Boolean

**Assert** `τ . = v(true)`

**Assert** `τ . = δ(false)`

**Assert** `τ . ≠ δ(null)`

**Assert** `τ . ≠ δ(invalid)`

**Assert** `τ . = v((null::('A)Boolean))`

**Assert** `τ . ≠ v(invalid)`

**Assert** `τ . = (true and true)`

**Assert** `τ . = (true and true . = true)`

**Assert** `τ . = ((null or null) . = null)`

**Assert** `τ . = ((null or null) . = null)`

**Assert** `τ . = ((true . = false) . = false)`

**Assert** `τ . = ((invalid . = false) . = false)`

**Assert** `τ . = ((invalid . = false) . = invalid)`

**Assert** `τ . = (true <> false)`

**Assert** `τ . = (false <> true)`

end

**theory** *UML-Void*

**imports** ../UML-PropertyProfiles

begin

## 2.3. Basic Type Void: Operations

This *minimal* OCL type contains only two elements: *invalid* and *null*. *Void* could initially be defined as `⟨⟨unit⟩⟩_⊥`, however the cardinal of this type is more than two, so it would have the cost to consider
Some None and Some (Some (Some ())) seemingly everywhere.

### 2.3.1. Fundamental Properties on Voids: Strict Equality

**Definition**

instantiation $Void_{base} :: bot$

begin

definition bot-Void-def: (bot-class bot :: Void_{base}) ≡ Abs-Void_{base} None

instance $\langle proof \rangle$

end

instantiation $Void_{base} :: null$

begin

definition null-Void-def: (null:: Void_{base}) ≡ Abs-Void_{base} None

instance $\langle proof \rangle$

end

The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar to the '$\mathcal{A}$ Void-case as strict extension of the strong equality:

def s (overloaded) StrictRefEq$_{Void}$[code-unfold] :

$$ 
\begin{align*}
(x::('\mathcal{A}) Void) \doteq y &\equiv \lambda \tau. \text{ if } (v x) \tau = \text{true } \tau \land (v y) \tau = \text{true } \tau \\
&\text{ then } (x \triangleq y) \tau \\
&\text{ else invalid } \tau
\end{align*}
$$

Property proof in terms of profile-bin$_{StrongEq^-v^-v}$

interpretation StrictRefEq$_{Void}$ : profile-bin$_{StrongEq^-v^-v}$ $\lambda x y$. $(x::('\mathcal{A}) Void) \doteq y$ $\langle proof \rangle$

### 2.3.2. Basic Void Constants

### 2.3.3. Validity and Definedness Properties

lemma $\delta (null::('\mathcal{A}) Void) = false \langle proof \rangle$

lemma $v (null::('\mathcal{A}) Void) = true \langle proof \rangle$

lemma $[simp,code-unfold]: \delta (\lambda-. \ Abs-Void_{base} None) = false$ $\langle proof \rangle$

lemma $[simp,code-unfold]: v (\lambda-. \ Abs-Void_{base} None) = false$ $\langle proof \rangle$

lemma $[simp,code-unfold]: \delta (\lambda-. \ Abs-Void_{base} None) = false$ $\langle proof \rangle$

lemma $[simp,code-unfold]: v (\lambda-. \ Abs-Void_{base} None) = true$ $\langle proof \rangle$

### 2.3.4. Test Statements

Assert $\tau \models ((null::('\mathcal{A}) Void) \doteq null)$

end
theory UML-Integer

imports ../UML-PropertyProfiles

begin

## 2.4. Basic Type Integer: Operations

### 2.4.1. Fundamental Predicates on Integers: Strict Equality

The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar to the 'A Boolean-case as strict extension of the strong equality:

defns (overloaded) StrictRefEqInteger [code-unfold] :

$$ (x::('A)Integer) \doteq y \equiv \lambda \tau. \text{ if } (v x) \tau = \text{true } \tau \land (v y) \tau = \text{true } \tau \\ \text{then } (x \triangleq y) \tau \\ \text{else invalid } \tau $$

Property proof in terms of profile-bin$_{StrongEq-v}$-v

interpretation StrictRefEqInteger : profile-bin$_{StrongEq-v}$-v $\lambda x$. (x::('A)Integer) $\doteq$ y
<proof>

### 2.4.2. Basic Integer Constants

Although the remaining part of this library reasons about integers abstractly, we provide here as example some convenient shortcuts.

definition OclInt0 :: ('A)Integer (0) where 0 = (λ - . . . 0::int$_{⊥}$)

definition OclInt1 :: ('A)Integer (1) where 1 = (λ - . . . 1::int$_{⊥}$)

definition OclInt2 :: ('A)Integer (2) where 2 = (λ - . . . 2::int$_{⊥}$)

Etc.

definition OclInt3 :: ('A)Integer (3) where 3 = (λ - . . . 3::int$_{⊥}$)

definition OclInt4 :: ('A)Integer (4) where 4 = (λ - . . . 4::int$_{⊥}$)

definition OclInt5 :: ('A)Integer (5) where 5 = (λ - . . . 5::int$_{⊥}$)

definition OclInt6 :: ('A)Integer (6) where 6 = (λ - . . . 6::int$_{⊥}$)

definition OclInt7 :: ('A)Integer (7) where 7 = (λ - . . . 7::int$_{⊥}$)

definition OclInt8 :: ('A)Integer (8) where 8 = (λ - . . . 8::int$_{⊥}$)

definition OclInt9 :: ('A)Integer (9) where 9 = (λ - . . . 9::int$_{⊥}$)

definition OclInt10 :: ('A)Integer (10) where 10 = (λ - . . . 10::int$_{⊥}$)

### 2.4.3. Validity and Definedness Properties

lemma δ (null::('A)Integer) = false <proof>

lemma v (null::('A)Integer) = true <proof>

lemma [simp, code-unfold]: δ (λ- . . . n$_{⊥}$) = true
<proof>

lemma [simp, code-unfold]: v (λ- . . . n$_{⊥}$) = true
<proof>

lemma [simp, code-unfold]: δ 0 = true <proof>

lemma [simp, code-unfold]: v 0 = true <proof>

lemma [simp, code-unfold]: δ 1 = true <proof>

lemma [simp, code-unfold]: v 1 = true <proof>
lemma [simp,code-unfold]: δ 2 = true <proof>

lemma [simp,code-unfold]: v 2 = true <proof>

lemma [simp,code-unfold]: δ 6 = true <proof>

lemma [simp,code-unfold]: v 6 = true <proof>

lemma [simp,code-unfold]: δ 8 = true <proof>

lemma [simp,code-unfold]: v 8 = true <proof>

lemma [simp,code-unfold]: δ 9 = true <proof>

lemma [simp,code-unfold]: v 9 = true <proof>

2.4.4. Arithmetical Operations

Definition

Here is a common case of a built-in operation on built-in types. Note that the arguments must be both
defined (non-null, non-bot).

Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these
operators are heavily overloaded in the HOL library that a further overloading would lead to heavy
technical buzz in this document.

definition **OclAddInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Integer (**infix** +<sub>int</sub> 40)

where $x +_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{true} \ \tau \wedge (\delta y) \tau = \text{true} \ \tau$

then ⏐^x τ^ + ⏐^y τ^ ⏐

else invalid τ

interpretation OclAddInteger : profile-bin<sub>d-d</sub> op +<sub>int</sub> λ x y. ⏐^x^ + ⏐^y^

<proof>

definition **OclMinusInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Integer (**infix** -<sub>int</sub> 41)

where $x -_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{true} \ \tau \wedge (\delta y) \tau = \text{true} \ \tau$

then ⏐^x τ^ - ⏐^y τ^ ⏐

else invalid τ

interpretation OclMinusInteger : profile-bin<sub>d-d</sub> op -<sub>int</sub> λ x y. ⏐^x^ - ⏐^y^

<proof>

definition **OclMultInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Integer (**infix** *<sub>int</sub>* 45)

where $x *_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{true} \ \tau \wedge (\delta y) \tau = \text{true} \ \tau$

then ⏐^x τ^ * ⏐^y τ^ ⏐

else invalid τ

interpretation OclMultInteger : profile-bin<sub>d-d</sub> op *<sub>int</sub>* λ x y. ⏐^x^ * ⏐^y^

<proof>

Here is the special case of division, which is defined as invalid for division by zero.

definition **OclDivisionInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Integer (**infix** div<sub>int</sub> 45)

where $x \div_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{true} \ \tau \wedge (\delta y) \tau = \text{true} \ \tau$

then if y τ ≠ OclInt0 τ then ⏐^x τ^ div ⏐^y τ^

else invalid τ

definition **OclModulusInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Integer (**infix** mod<sub>int</sub> 45)

where $x \bmod_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{true} \ \tau \wedge (\delta y) \tau = \text{true} \ \tau$

then if y τ ≠ OclInt0 τ then ⏐^x τ^ mod ⏐^y τ^

else invalid τ

definition **OclLessInteger** ::= ('A)Integer ⇒ ('A)Integer ⇒ ('A)Boolean (**infix** <<sub>int</sub> 35)
where $x <_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{ true } \tau \land (\delta y) \tau = \text{ true } \tau$
then $\underset{\perp}{\top} x \tau^{\top} < \underset{\perp}{\top} y \tau^{\top}$
else invalid $\tau$

interpretation $OclLess_{Integer}: \text{profile-bin}_{d-d} \text{ op} <_{int} \lambda x y. \underset{\perp}{\top} x^{\top} < \underset{\perp}{\top} y^{\top}$
$\langle\text{proof}\rangle$

definition $OclLe_{Integer} :: ('\mathfrak{A})Integer \Rightarrow ('\mathfrak{A})Integer \Rightarrow ('\mathfrak{A})Boolean$ **(infix $\leq_{int}$ 35)**

where $x \leq_{int} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{ true } \tau \land (\delta y) \tau = \text{ true } \tau$
then $\underset{\perp}{\top} x \tau^{\top} \leq \underset{\perp}{\top} y \tau^{\top}$
else invalid $\tau$

interpretation $OclLe_{Integer}: \text{profile-bin}_{d-d} \text{ op} \leq_{int} \lambda x y. \underset{\perp}{\top} x^{\top} \leq \underset{\perp}{\top} y^{\top}$
$\langle\text{proof}\rangle$

## Basic Properties

lemma $OclAdd_{Integer}$-commute: $(X +_{int} Y) = (Y +_{int} X)$
$\langle\text{proof}\rangle$

## Execution with Invalid or Null or Zero as Argument

lemma $OclAdd_{Integer}$-zero1 [simp, code-unfold] :
$(x +_{int} 0) = (\text{if } v \text{ x and not } (\delta x) \text{ then invalid else } x \text{ endif})$
$\langle\text{proof}\rangle$

lemma $OclAdd_{Integer}$-zero2 [simp, code-unfold] :
$(\mathbf{0} +_{int} x) = (\text{if } v \text{ x and not } (\delta x) \text{ then invalid else } x \text{ endif})$
$\langle\text{proof}\rangle$

## 2.4.5. Test Statements

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to True.

Assert $\tau \models (\mathbf{9} \leq_{int} \mathbf{10})$

Assert $\tau \models ((\mathbf{4} +_{int} \mathbf{4}) \leq_{int} \mathbf{10})$

Assert $\tau \not\models ((\mathbf{4} +_{int} (\mathbf{4} +_{int} \mathbf{4})) <_{int} \mathbf{10})$

Assert $\tau \models \text{ not } (v (\mathbf{null} +_{int} \mathbf{1}))$

Assert $\tau \models (((\mathbf{9} *_{int} \mathbf{4}) \text{ div}_{int} \mathbf{10}) \leq_{int} \mathbf{4})$

Assert $\tau \models \text{ not } (\delta (\mathbf{1} \text{ div}_{int} \mathbf{0}))$

Assert $\tau \models \text{ not } (v (\mathbf{1} \text{ div}_{int} \mathbf{0}))$

lemma integer-non-null [simp]: (((\lambda-. \underset{\perp}{\top} n_{\perp})) \doteq (null::('\mathfrak{A})Integer)) = false
$\langle\text{proof}\rangle$

lemma null-non-integer [simp]: (((null::('\mathfrak{A})Integer) \doteq (\lambda-. \underset{\perp}{\top} n_{\perp})) = false
$\langle\text{proof}\rangle$

lemma OclInt0-non-null [simp, code-unfold]: (\mathbf{0} \doteq \mathbf{null}) = false $\langle\text{proof}\rangle$

lemma null-non-OclInt0 [simp, code-unfold]: (null \doteq \mathbf{0}) = false $\langle\text{proof}\rangle$

lemma OclInt1-non-null [simp, code-unfold]: (\mathbf{1} \doteq \mathbf{null}) = false $\langle\text{proof}\rangle$

lemma null-non-OclInt1 [simp, code-unfold]: (null \doteq \mathbf{1}) = false $\langle\text{proof}\rangle$

lemma OclInt2-non-null [simp, code-unfold]: (\mathbf{2} \doteq \mathbf{null}) = false $\langle\text{proof}\rangle$

lemma null-non-OclInt2 [simp, code-unfold]: (null \doteq \mathbf{2}) = false $\langle\text{proof}\rangle$

lemma OclInt6-non-null [simp, code-unfold]: (\mathbf{6} \doteq \mathbf{null}) = false $\langle\text{proof}\rangle$

lemma null-non-OclInt6 [simp, code-unfold]: (null \doteq \mathbf{6}) = false $\langle\text{proof}\rangle$

lemma OclInt8-non-null [simp, code-unfold]: (\mathbf{8} \doteq \mathbf{null}) = false $\langle\text{proof}\rangle$
lemma null-non-OclInt8 [simp,code-unfold]: (null = 8) = false `proof`

lemma OclInt9-non-null [simp,code-unfold]: (9 = null) = false `proof`

lemma null-non-OclInt9 [simp,code-unfold]: (null = 9) = false `proof`

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to True.

Elementary computations on Integer

Assert τ |= ((0 <$_{int}$ 2) and (0 <$_{int}$ 1))

Assert τ |= 1 <> 2

Assert τ |= 2 <> 1

Assert τ |= 2 = 2

Assert τ |= v 4

Assert τ |= δ 4

Assert τ |= v (null::('A)Integer)

Assert τ |= (invalid = invalid)

Assert τ |= (null = null)

Assert τ |= (4 = 4)

Assert τ |:= (9 = 10)

Assert τ |:= (invalid = 10)

Assert τ |:= (null = 10)

Assert τ |:= (invalid = (invalid::('A)Integer))

Assert τ |:= v (invalid = (invalid::('A)Integer))

Assert τ |:= (invalid <> (invalid::('A)Integer))

Assert τ |:= v (invalid <> (invalid::('A)Integer)))

Assert τ |= (null = (null::('A)Integer))

Assert τ |= (null = (null::('A)Integer))

Assert τ |= (4 = 4)

Assert τ |:= (4 <> 4)

Assert τ |:= (4 = 10)

Assert τ |= (4 <> 10)

Assert τ |:= (0 <$_{int}$ null)

Assert τ |:= (δ (0 <$_{int}$ null))

end

theory UML-Real

imports ../UML-PropertyProfiles

begin

## 2.5. Basic Type Real: Operations

### 2.5.1. Fundamental Predicates on Reals: Strict Equality

The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar to the 'A Boolean -case as strict extension of the strong equality:

def s (overloaded) StrictRefEqqReal [code-unfold] :

$$
\begin{align*}
(x::('A)Real) \doteq & y \equiv \lambda \tau. \text{ if } (v x) \tau = \text{true } \tau \land (v y) \tau = \text{true } \tau \\
& \text{then } (x \triangleq y) \tau \\
& \text{else invalid } \tau
\end{align*}
$$

Property proof in terms of profile-bin$_{StrongEq}$-$v$-$v$
interpretation StrictRefEqReal : profile-binStrongEq-v-v λ x y. (x::('A)Real) = y
<proof>

## 2.5.2. Basic Real Constants

Although the remaining part of this library reasons about reals abstractly, we provide here as example some convenient shortcuts.

definition OclReal0 ::('A)Real (0.0) where 0.0 = (λ - . . . 0::real_↓)

definition OclReal1 ::('A)Real (1.0) where 1.0 = (λ - . . . 1::real_↓)

definition OclReal2 ::('A)Real (2.0) where 2.0 = (λ - . . . 2::real_↓)

Etc.

definition OclReal3 ::('A)Real (3.0) where 3.0 = (λ - . . . 3::real_↓)

definition OclReal4 ::('A)Real (4.0) where 4.0 = (λ - . . . 4::real_↓)

definition OclReal5 ::('A)Real (5.0) where 5.0 = (λ - . . . 5::real_↓)

definition OclReal6 ::('A)Real (6.0) where 6.0 = (λ - . . . 6::real_↓)

definition OclReal7 ::('A)Real (7.0) where 7.0 = (λ - . . . 7::real_↓)

definition OclReal8 ::('A)Real (8.0) where 8.0 = (λ - . . . 8::real_↓)

definition OclReal9 ::('A)Real (9.0) where 9.0 = (λ - . . . 9::real_↓)

definition OclReal10 ::('A)Real (10.0) where 10.0 = (λ - . . . 10::real_↓)

definition OclRealpi ::('A)Real (π) where π = (λ - . . . pi_↓)

## 2.5.3. Validity and Definedness Properties

lemma δ(null::('A)Real) = false <proof>

lemma v(null::('A)Real) = true <proof>

lemma [simp, code-unfold]: δ (λ- . . n_↓) = true <proof>

lemma [simp, code-unfold]: v (λ- . . n_↓) = true <proof>

lemma [simp, code-unfold]: δ 0.0 = true <proof>

lemma [simp, code-unfold]: v 0.0 = true <proof>

lemma [simp, code-unfold]: δ 1.0 = true <proof>

lemma [simp, code-unfold]: v 1.0 = true <proof>

lemma [simp, code-unfold]: δ 2.0 = true <proof>

lemma [simp, code-unfold]: v 2.0 = true <proof>

lemma [simp, code-unfold]: δ 6.0 = true <proof>

lemma [simp, code-unfold]: v 6.0 = true <proof>

lemma [simp, code-unfold]: δ 8.0 = true <proof>

lemma [simp, code-unfold]: v 8.0 = true <proof>

lemma [simp, code-unfold]: δ 9.0 = true <proof>

lemma [simp, code-unfold]: v 9.0 = true <proof>

## 2.5.4. Arithmetical Operations

### Definition

Here is a common case of a built-in operation on built-in types. Note that the arguments must be both defined (non-null, non-bot).

Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these operators are heavily overloaded in the HOL library that a further overloading would lead to heavy technical buzz in this document.
**definition** $\mathit{OclAdd}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \ (\mathbf{infix} \ +_{\mathit{real}} \ 40)$

**where** $x +_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then $\sqcup^\top x \tau^\top + \sqcup^\top y \tau^\top \sqcup$
\qquad else invalid $\tau$

**interpretation** $\mathit{OclAdd}_{\mathit{Real}} : \mathit{profile-bin}_d \mathit{d} \ op +_{\mathit{real}} \lambda x y. \ \sqcup^\top x^\top + \sqcup^\top y^\top \sqcup$
$\langle \mathit{proof} \rangle$

**definition** $\mathit{OclMinus}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \ (\mathbf{infix} \ -_{\mathit{real}} \ 41)$

**where** $x -_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then $\sqcup^\top x \tau^\top - \sqcup^\top y \tau^\top \sqcup$
\qquad else invalid $\tau$

**interpretation** $\mathit{OclMinus}_{\mathit{Real}} : \mathit{profile-bin}_d \mathit{d} \ op -_{\mathit{real}} \lambda x y. \ \sqcup^\top x^\top - \sqcup^\top y^\top \sqcup$
$\langle \mathit{proof} \rangle$

**definition** $\mathit{OclMult}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \ (\mathbf{infix} \ *_{\mathit{real}} \ 45)$

**where** $x *_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then $\sqcup^\top x \tau^\top * \sqcup^\top y \tau^\top \sqcup$
\qquad else invalid $\tau$

**interpretation** $\mathit{OclMult}_{\mathit{Real}} : \mathit{profile-bin}_d \mathit{d} \ op *_{\mathit{real}} \lambda x y. \ \sqcup^\top x^\top * \sqcup^\top y^\top \sqcup$
$\langle \mathit{proof} \rangle$

Here is the special case of division, which is defined as invalid for division by zero.

**definition** $\mathit{OclDivision}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \ (\mathbf{infix} \ div_{\mathit{real}} \ 45)$

**where** $x \ div_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then if $y \tau \neq \mathit{OclReal0} \ \tau$ then $\sqcup^\top x \tau^\top / \sqcup^\top y \tau^\top \sqcup$ else invalid $\tau$
\qquad else invalid $\tau$

**definition** $\mathit{mod}-\mathit{float} \ a \ b = a - \mathit{real} \ (\mathit{floor} \ (a / b)) * b$

**definition** $\mathit{OclModulus}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \ (\mathbf{infix} \ mod_{\mathit{real}} \ 45)$

**where** $x \ mod_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then if $y \tau \neq \mathit{OclReal0} \ \tau$ then $\sqcup \mathit{mod}-\mathit{float} \ \sqcup^\top x \tau^\top \sqcup^\top y \tau^\top \sqcup$ else invalid $\tau$
\qquad else invalid $\tau$

**definition** $\mathit{OclLess}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Boolean} \ (\mathbf{infix} \ <_{\mathit{real}} \ 35)$

**where** $x <_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then $\sqcup^\top x \tau^\top < \sqcup^\top y \tau^\top \sqcup$
\qquad else invalid $\tau$

**interpretation** $\mathit{OclLess}_{\mathit{Real}} : \mathit{profile-bin}_d \mathit{d} \ op <_{\mathit{real}} \lambda x y. \ \sqcup^\top x^\top < \sqcup^\top y^\top \sqcup$
$\langle \mathit{proof} \rangle$

**definition** $\mathit{OclLe}_{\mathit{Real}} :: (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Real} \Rightarrow (\mathfrak{A})\mathit{Boolean} \ (\mathbf{infix} \ \leq_{\mathit{real}} \ 35)$

**where** $x \leq_{\mathit{real}} y \equiv \lambda \tau. \ \mathit{if} \ (\delta x) \ \tau = \mathit{true} \ \tau \wedge \ (\delta y) \ \tau = \mathit{true} \ \tau$
\qquad then $\sqcup^\top x \tau^\top \leq^\top y \tau^\top \sqcup$
\qquad else invalid $\tau$

**interpretation** $\mathit{OclLe}_{\mathit{Real}} : \mathit{profile-bin}_d \mathit{d} \ op \leq_{\mathit{real}} \lambda x y. \ \sqcup^\top x^\top \leq^\top y^\top \sqcup$
$\langle \mathit{proof} \rangle$

## Basic Properties

**lemma** $\mathit{OclAdd}_{\mathit{Real}}$-commute: $(X +_{\mathit{real}} Y) = (Y +_{\mathit{real}} X)$
$\langle \mathit{proof} \rangle$
### Execution with Invalid or Null or Zero as Argument

**lemma OclAddReal-zero1 [simp, code-unfold] :**
$$ (x +_{real} 0.0) = (\text{if } v \text{ x and not } (\delta x) \text{ then invalid else } x \text{ else if } \langle\text{proof}\rangle ) $$

**lemma OclAddReal-zero2 [simp, code-unfold] :**
$$ (0.0 +_{real} x) = (\text{if } v \text{ x and not } (\delta x) \text{ then invalid else } x \text{ else if } \langle\text{proof}\rangle ) $$

## 2.5.5. Test Statements

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to True.

**Assert** $\tau \models ( 9.0 \leq_{real} 10.0 )$

**Assert** $\tau \models (( 4.0 +_{real} 4.0 ) \leq_{real} 10.0 )$

**Assert** $\tau \not\models (( 4.0 +_{real} ( 4.0 +_{real} 4.0 ) ) <_{real} 10.0 )$

**Assert** $\tau \models \text{not } (v (\text{null} +_{real} 1.0))$

**Assert** $\tau \models (((9.0 *_{real} 4.0) \text{div}_{real} 10.0) \leq_{real} 4.0)$

**Assert** $\tau \models \text{not } (\delta (1.0 \text{div}_{real} 0.0))$

**Assert** $\tau \models \text{not } (v (1.0 \text{div}_{real} 0.0))$

**lemma** real-non-null [simp]: $((\lambda-. \llcorner n \llcorner \rangle) \doteq (\text{null}::('\mathfrak{A})\text{Real})) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-real [simp]: $((\text{null}::('\mathfrak{A})\text{Real}) \doteq (\lambda-. \llcorner n \llcorner \rangle)) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal0-non-null [simp, code-unfold]: $(0.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal0 [simp, code-unfold]: $(\text{null} \doteq 0.0) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal1-non-null [simp, code-unfold]: $(1.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal1 [simp, code-unfold]: $(\text{null} \doteq 1.0) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal2-non-null [simp, code-unfold]: $(2.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal2 [simp, code-unfold]: $(\text{null} \doteq 2.0) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal6-non-null [simp, code-unfold]: $(6.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal6 [simp, code-unfold]: $(\text{null} \doteq 6.0) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal8-non-null [simp, code-unfold]: $(8.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal8 [simp, code-unfold]: $(\text{null} \doteq 8.0) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** OclReal9-non-null [simp, code-unfold]: $(9.0 \doteq \text{null}) = \text{false} \quad \langle\text{proof}\rangle$

**lemma** null-non-OclReal9 [simp, code-unfold]: $(\text{null} \doteq 9.0) = \text{false} \quad \langle\text{proof}\rangle$

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to True.

### Elementary computations on Real

**Assert** $\tau \models 1.0 \prec \prec 2.0$

**Assert** $\tau \models 2.0 \prec \prec 1.0$

**Assert** $\tau \models 2.0 \doteq 2.0$

**Assert** $\tau \models v 4.0$

**Assert** $\tau \models \delta 4.0$

**Assert** $\tau \models v (\text{null}::('\mathfrak{A})\text{Real})$

**Assert** $\tau \models (\text{invalid} \triangleq \text{invalid})$

**Assert** $\tau \models (\text{null} \triangleq \text{null})$

**Assert** $\tau \models (4.0 \triangleq 4.0)$

**Assert** $\tau \not\models (9.0 \triangleq 10.0)$