# Theory OCL_Examples

(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
chapter ‹Examples›
theory OCL_Examples
imports OCL_Normalization
begin

(*** Classes ****************************************************************)

section ‹Classes›

datatype classes1 =
Object | Person | Employee | Customer | Project | Task | Sprint

inductive subclass1 where
"c ≠ Object ⟹
subclass1 c Object"
| "subclass1 Employee Person"
| "subclass1 Customer Person"

instantiation classes1 :: semilattice_sup
begin

definition "(<) ≡ subclass1"
definition "(≤) ≡ subclass1⇧=⇧="

fun sup_classes1 where
"Object ⊔ _ = Object"
| "Person ⊔ c = (if c = Person ∨ c = Employee ∨ c = Customer
then Person else Object)"
| "Employee ⊔ c = (if c = Employee then Employee else
if c = Person ∨ c = Customer then Person else Object)"
| "Customer ⊔ c = (if c = Customer then Customer else
if c = Person ∨ c = Employee then Person else Object)"
| "Project ⊔ c = (if c = Project then Project else Object)"
| "Sprint ⊔ c = (if c = Sprint then Sprint else Object)"

lemma less_le_not_le_classes1:
"c < d ⟷ c ≤ d ∧ ¬ d ≤ c"
for c d :: classes1
unfolding less_classes1_def less_eq_classes1_def
using subclass1.simps by auto

lemma order_refl_classes1:
"c ≤ c"
for c :: classes1
unfolding less_eq_classes1_def by simp

lemma order_trans_classes1:
"c ≤ d ⟹ d ≤ e ⟹ c ≤ e"
for c d e :: classes1
unfolding less_eq_classes1_def
using subclass1.simps by auto

lemma antisym_classes1:
"c ≤ d ⟹ d ≤ c ⟹ c = d"
for c d :: classes1
unfolding less_eq_classes1_def
using subclass1.simps by auto

lemma sup_ge1_classes1:
"c ≤ c ⊔ d"
for c d :: classes1
by (induct c; auto simp add: less_eq_classes1_def less_classes1_def subclass1.simps)

lemma sup_ge2_classes1:
"d ≤ c ⊔ d"
for c d :: classes1
by (induct c; auto simp add: less_eq_classes1_def less_classes1_def subclass1.simps)

lemma sup_least_classes1:
"c ≤ e ⟹ d ≤ e ⟹ c ⊔ d ≤ e"
for c d e :: classes1
by (induct c; induct d;
auto simp add: less_eq_classes1_def less_classes1_def subclass1.simps)

instance
apply intro_classes
apply (rule order_trans_classes1; auto)

end

code_pred subclass1 .

fun subclass1_fun where
"subclass1_fun Object 𝒞 = False"
| "subclass1_fun Person 𝒞 = (𝒞 = Object)"
| "subclass1_fun Employee 𝒞 = (𝒞 = Object ∨ 𝒞 = Person)"
| "subclass1_fun Customer 𝒞 = (𝒞 = Object ∨ 𝒞 = Person)"
| "subclass1_fun Project 𝒞 = (𝒞 = Object)"
| "subclass1_fun Task 𝒞 = (𝒞 = Object)"
| "subclass1_fun Sprint 𝒞 = (𝒞 = Object)"

lemma less_classes1_code [code]:
"(<) = subclass1_fun"
proof (intro ext iffI)
fix 𝒞 𝒟 :: "classes1"
show "𝒞 < 𝒟 ⟹ subclass1_fun 𝒞 𝒟"
unfolding less_classes1_def
apply (erule subclass1.cases, auto)
using subclass1_fun.elims(3) by blast
show "subclass1_fun 𝒞 𝒟 ⟹ 𝒞 < 𝒟"
by (erule subclass1_fun.elims, auto simp add: less_classes1_def subclass1.intros)
qed

lemma less_eq_classes1_code [code]:
"(≤) = (λx y. subclass1_fun x y ∨ x = y)"
unfolding dual_order.order_iff_strict less_classes1_code
by auto

(*** Object Model ***********************************************************)

section ‹Object Model›

abbreviation "Γ⇩0 ≡ fmempty :: classes1 type env"
declare [[coercion "ObjectType :: classes1 ⇒ classes1 basic_type"]]
declare [[coercion "phantom :: String.literal ⇒ classes1 enum"]]

instantiation classes1 :: ocl_object_model
begin

definition "classes_classes1 ≡
{|Object, Person, Employee, Customer, Project, Task, Sprint|}"

definition "attributes_classes1 ≡ fmap_of_list [
(Person, fmap_of_list [
(STR ''name'', String[1] :: classes1 type)]),
(Employee, fmap_of_list [
(STR ''name'', String[1]),
(STR ''position'', String[1])]),
(Customer, fmap_of_list [
(STR ''vip'', Boolean[1])]),
(Project, fmap_of_list [
(STR ''name'', String[1]),
(STR ''cost'', Real[?])]),
(STR ''description'', String[1])])]"

abbreviation "assocs ≡ [
STR ''ProjectManager'' ↦⇩f [
STR ''projects'' ↦⇩f (Project, 0::nat, ∞::enat, False, True),
STR ''manager'' ↦⇩f (Employee, 1, 1, False, False)],
STR ''ProjectMember'' ↦⇩f [
STR ''member_of'' ↦⇩f (Project, 0, ∞, False, False),
STR ''members'' ↦⇩f (Employee, 1, 20, True, True)],
STR ''ManagerEmployee'' ↦⇩f [
STR ''line_manager'' ↦⇩f (Employee, 0, 1, False, False),
STR ''project_manager'' ↦⇩f (Employee, 0, ∞, False, False),
STR ''employees'' ↦⇩f (Employee, 3, 7, False, False)],
STR ''ProjectCustomer'' ↦⇩f [
STR ''projects'' ↦⇩f (Project, 0, ∞, False, True),
STR ''customer'' ↦⇩f (Customer, 1, 1, False, False)],
STR ''project'' ↦⇩f (Project, 1, 1, False, False),
STR ''sprint'' ↦⇩f (Sprint, 0, 10, False, True),
STR ''assignee'' ↦⇩f (Employee, 0, 1, False, False)]]"

definition "associations_classes1 ≡ assocs"

definition "association_classes_classes1 ≡ fmempty :: classes1 ⇀⇩f assoc"

text ‹
\begin{verbatim}
context Project
def: membersCount() : Integer[1] = members->size()
def: membersByName(mn : String[1]) : Set(Employee[1]) =
members->select(member | member.name = mn)
static def: allProjects() : Set(Project[1]) =
Project[1].allInstances()
\end{verbatim}›

definition "operations_classes1 ≡ [
(STR ''membersCount'', Project[1], [], Integer[1], False,
Some (OperationCall
(AssociationEndCall (Var STR ''self'') DotCall None STR ''members'')
ArrowCall CollectionSizeOp [])),
(STR ''membersByName'', Project[1], [(STR ''mn'', String[1], In)],
Set Employee[1], False,
Some (SelectIteratorCall
(AssociationEndCall (Var STR ''self'') DotCall None STR ''members'')
ArrowCall [STR ''member''] None
(OperationCall
(AttributeCall (Var STR ''member'') DotCall STR ''name'')
DotCall EqualOp [Var STR ''mn'']))),
(STR ''allProjects'', Project[1], [], Set Project[1], True,
Some (MetaOperationCall Project[1] AllInstancesOp))
] :: (classes1 type, classes1 expr) oper_spec list"

definition "literals_classes1 ≡ fmap_of_list [
(STR ''E1'' :: classes1 enum, {|STR ''A'', STR ''B''|}),
(STR ''E2'', {|STR ''C'', STR ''D'', STR ''E''|})]"

lemma assoc_end_min_less_eq_max:
"assoc |∈| fmdom assocs ⟹
fmlookup assocs assoc = Some ends ⟹
role |∈| fmdom ends  ⟹
fmlookup ends role = Some end ⟹
assoc_end_min end ≤ assoc_end_max end"
unfolding assoc_end_min_def assoc_end_max_def
using zero_enat_def one_enat_def numeral_eq_enat by auto

lemma association_ends_unique:
assumes "association_ends' classes assocs 𝒞 from role end⇩1"
and "association_ends' classes assocs 𝒞 from role end⇩2"
shows "end⇩1 = end⇩2"
proof -
have "¬ association_ends_not_unique' classes assocs" by eval
with assms show ?thesis
using association_ends_not_unique'.simps by blast
qed

instance
apply standard
unfolding associations_classes1_def
using assoc_end_min_less_eq_max apply blast
using association_ends_unique by blast

end

(*** Simplification Rules ***************************************************)

section ‹Simplification Rules›

lemma ex_alt_simps [simp]:
"∃a. a"
"∃a. ¬ a"
"(∃a. (a ⟶ P) ∧ a) = P"
"(∃a. ¬ a ∧ (¬ a ⟶ P)) = P"
by auto

declare numeral_eq_enat [simp]

lemmas basic_type_le_less [simp] = Orderings.order_class.le_less
for x y :: "'a basic_type"

declare element_type_alt_simps [simp]
declare update_element_type.simps [simp]
declare to_unique_collection.simps [simp]
declare to_nonunique_collection.simps [simp]
declare to_ordered_collection.simps [simp]

declare assoc_end_class_def [simp]
declare assoc_end_min_def [simp]
declare assoc_end_max_def [simp]
declare assoc_end_ordered_def [simp]
declare assoc_end_unique_def [simp]

declare oper_name_def [simp]
declare oper_context_def [simp]
declare oper_params_def [simp]
declare oper_result_def [simp]
declare oper_static_def [simp]
declare oper_body_def [simp]

declare oper_in_params_def [simp]
declare oper_out_params_def [simp]

declare assoc_end_type_def [simp]
declare oper_type_def [simp]

declare op_type_alt_simps [simp]
declare typing_alt_simps [simp]
declare normalize_alt_simps [simp]
declare nf_typing.simps [simp]

declare subclass1.intros [intro]
declare less_classes1_def [simp]

declare literals_classes1_def [simp]

lemma attribute_Employee_name [simp]:
"attribute Employee STR ''name'' 𝒟 τ =
(𝒟 = Employee ∧ τ = String[1])"
proof -
have "attribute Employee STR ''name'' Employee String[1]"
by eval
thus ?thesis
using attribute_det by blast
qed

lemma association_end_Project_members [simp]:
"association_end Project None STR ''members'' 𝒟 τ =
(𝒟 = Project ∧ τ = (Employee, 1, 20, True, True))"
proof -
have "association_end Project None STR ''members''
Project (Employee, 1, 20, True, True)"
by eval
thus ?thesis
using association_end_det by blast
qed

lemma association_end_Employee_projects_simp [simp]:
"association_end Employee None STR ''projects'' 𝒟 τ =
(𝒟 = Employee ∧ τ = (Project, 0, ∞, False, True))"
proof -
have "association_end Employee None STR ''projects''
Employee (Project, 0, ∞, False, True)"
by eval
thus ?thesis
using association_end_det by blast
qed

lemma static_operation_Project_allProjects [simp]:
"static_operation ⟨Project⟩⇩𝒯[1] STR ''allProjects'' [] oper =
(oper = (STR ''allProjects'', ⟨Project⟩⇩𝒯[1], [], Set ⟨Project⟩⇩𝒯[1], True,
Some (MetaOperationCall ⟨Project⟩⇩𝒯[1] AllInstancesOp)))"
proof -
have "static_operation ⟨Project⟩⇩𝒯[1] STR ''allProjects'' []
(STR ''allProjects'', ⟨Project⟩⇩𝒯[1], [], Set ⟨Project⟩⇩𝒯[1], True,
Some (MetaOperationCall ⟨Project⟩⇩𝒯[1] AllInstancesOp))"
by eval
thus ?thesis
using static_operation_det by blast
qed

(*** Basic Types ************************************************************)

section ‹Basic Types›

subsection ‹Positive Cases›

lemma "UnlimitedNatural < (Real :: classes1 basic_type)" by simp
lemma "⟨Employee⟩⇩𝒯 < ⟨Person⟩⇩𝒯" by auto
lemma "⟨Person⟩⇩𝒯 ≤ OclAny" by simp

subsection ‹Negative Cases›

lemma "¬ String ≤ (Boolean :: classes1 basic_type)" by simp

(*** Types ******************************************************************)

section ‹Types›

subsection ‹Positive Cases›

lemma "Integer[?] < (OclSuper :: classes1 type)" by simp
lemma "Collection Real[?] < (OclSuper :: classes1 type)" by simp
lemma "Set (Collection Boolean[1]) < (OclSuper :: classes1 type)" by simp
lemma "Set (Bag Boolean[1]) < Set (Collection Boolean[?] :: classes1 type)"
by simp
lemma "Tuple (fmap_of_list [(STR ''a'', Boolean[1]), (STR ''b'', Integer[1])]) <
Tuple (fmap_of_list [(STR ''a'', Boolean[?] :: classes1 type)])" by eval

lemma "Integer[1] ⊔ (Real[?] :: classes1 type) = Real[?]" by simp
lemma "Set Integer[1] ⊔ Set (Real[1] :: classes1 type) = Set Real[1]" by simp
lemma "Set Integer[1] ⊔ Bag (Boolean[?] :: classes1 type) = Collection OclAny[?]"
by simp
lemma "Set Integer[1] ⊔ (Real[1] :: classes1 type) = OclSuper" by simp

subsection ‹Negative Cases›

lemma "¬ OrderedSet Boolean[1] < Set (Boolean[1] :: classes1 type)" by simp

(*** Typing *****************************************************************)

section ‹Typing›

subsection ‹Positive Cases›

text ‹
▩‹E1::A : E1[1]››
lemma
"Γ⇩0 ⊢ EnumLiteral STR ''E1'' STR ''A'' : (Enum STR ''E1'')[1]"
by simp

text ‹
▩‹true or false : Boolean[1]››
lemma
"Γ⇩0 ⊢ OperationCall (BooleanLiteral True) DotCall OrOp
[BooleanLiteral False] : Boolean[1]"
by simp

text ‹
▩‹null and true : Boolean[?]››
lemma
"Γ⇩0 ⊢ OperationCall (NullLiteral) DotCall AndOp
[BooleanLiteral True] : Boolean[?]"
by simp

text ‹
▩‹let x : Real[1] = 5 in x + 7 : Real[1]››
lemma
"Γ⇩0 ⊢ Let (STR ''x'') (Some Real[1]) (IntegerLiteral 5)
(OperationCall (Var STR ''x'') DotCall PlusOp [IntegerLiteral 7]) : Real[1]"
by simp

text ‹
▩‹null.oclIsUndefined() : Boolean[1]››
lemma
"Γ⇩0 ⊢ OperationCall (NullLiteral) DotCall OclIsUndefinedOp [] : Boolean[1]"
by simp

text ‹
▩‹Sequence{1..5, null}.oclIsUndefined() : Sequence(Boolean[1])››
lemma
"Γ⇩0 ⊢ OperationCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5),
CollectionItem NullLiteral])
DotCall OclIsUndefinedOp [] : Sequence Boolean[1]"
by simp

text ‹
▩‹Sequence{1..5}->product(Set{'a', 'b'})
: Set(Tuple(first: Integer[1], second: String[1]))››
lemma
"Γ⇩0 ⊢ OperationCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5)])
ArrowCall ProductOp
[CollectionLiteral SetKind
[CollectionItem (StringLiteral ''a''),
CollectionItem (StringLiteral ''b'')]] :
Set (Tuple (fmap_of_list [
(STR ''first'', Integer[1]), (STR ''second'', String[1])]))"
by simp

text ‹
▩‹Sequence{1..5, null}?->iterate(x, acc : Real[1] = 0 | acc + x)
: Real[1]››
lemma
"Γ⇩0 ⊢ IterateCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5),
CollectionItem NullLiteral]) SafeArrowCall
[STR ''x''] None
(STR ''acc'') (Some Real[1]) (IntegerLiteral 0)
(OperationCall (Var STR ''acc'') DotCall PlusOp [Var STR ''x'']) : Real[1]"
by simp

text ‹
▩‹Sequence{1..5, null}?->max() : Integer[1]››
lemma
"Γ⇩0 ⊢ OperationCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5),
CollectionItem NullLiteral])
SafeArrowCall CollectionMaxOp [] : Integer[1]"
by simp

text ‹
▩‹let x : Sequence(String[?]) = Sequence{'abc', 'zxc'} in
x->any(it | it = 'test') : String[?]››
lemma
"Γ⇩0 ⊢ Let (STR ''x'') (Some (Sequence String[?]))
(CollectionLiteral SequenceKind
[CollectionItem (StringLiteral ''abc''),
CollectionItem (StringLiteral ''zxc'')])
(AnyIteratorCall (Var STR ''x'') ArrowCall
[STR ''it''] None
(OperationCall (Var STR ''it'') DotCall EqualOp
[StringLiteral ''test''])) : String[?]"
by simp

text ‹
▩‹let x : Sequence(String[?]) = Sequence{'abc', 'zxc'} in
x?->closure(it | it) : OrderedSet(String[1])››
lemma
"Γ⇩0 ⊢ Let STR ''x'' (Some (Sequence String[?]))
(CollectionLiteral SequenceKind
[CollectionItem (StringLiteral ''abc''),
CollectionItem (StringLiteral ''zxc'')])
(ClosureIteratorCall (Var STR ''x'') SafeArrowCall
[STR ''it''] None
(Var STR ''it'')) : OrderedSet String[1]"
by simp

text ‹
▩‹context Employee:
name : String[1]››
lemma
"Γ⇩0(STR ''self'' ↦⇩f Employee[1]) ⊢
AttributeCall (Var STR ''self'') DotCall STR ''name'' : String[1]"
by simp

text ‹
▩‹context Employee:
projects : Set(Project[1])››
lemma
"Γ⇩0(STR ''self'' ↦⇩f Employee[1]) ⊢
AssociationEndCall (Var STR ''self'') DotCall None
STR ''projects'' : Set Project[1]"
by simp

text ‹
▩‹context Employee:
projects.members : Bag(Employee[1])››
lemma
"Γ⇩0(STR ''self'' ↦⇩f Employee[1]) ⊢
AssociationEndCall (AssociationEndCall (Var STR ''self'')
DotCall None STR ''projects'')
DotCall None STR ''members'' : Bag Employee[1]"
by simp

text ‹
▩‹Project[?].allInstances() : Set(Project[?])››
lemma
"Γ⇩0 ⊢ MetaOperationCall Project[?] AllInstancesOp : Set Project[?]"
by simp

text ‹
▩‹Project[1]::allProjects() : Set(Project[1])››
lemma
"Γ⇩0 ⊢ StaticOperationCall Project[1] STR ''allProjects'' [] : Set Project[1]"
by simp

subsection ‹Negative Cases›

text ‹
▩‹true = null››
lemma
"∄τ. Γ⇩0 ⊢ OperationCall (BooleanLiteral True) DotCall EqualOp
[NullLiteral] : τ"
by simp

text ‹
▩‹let x : Boolean[1] = 5 in x and true››
lemma
"∄τ. Γ⇩0 ⊢ Let STR ''x'' (Some Boolean[1]) (IntegerLiteral 5)
(OperationCall (Var STR ''x'') DotCall AndOp [BooleanLiteral True]) : τ"
by simp

text ‹
▩‹let x : Sequence(String[?]) = Sequence{'abc', 'zxc'} in
x->closure(it | 1)››
lemma
"∄τ. Γ⇩0 ⊢ Let STR ''x'' (Some (Sequence String[?]))
(CollectionLiteral SequenceKind
[CollectionItem (StringLiteral ''abc''),
CollectionItem (StringLiteral ''zxc'')])
(ClosureIteratorCall (Var STR ''x'') ArrowCall [STR ''it''] None
(IntegerLiteral 1)) : τ"
by simp

text ‹
▩‹Sequence{1..5, null}->max()››
lemma
"∄τ. Γ⇩0 ⊢ OperationCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5),
CollectionItem NullLiteral])
ArrowCall CollectionMaxOp [] : τ"
proof -
have "¬ operation_defined (Integer[?] :: classes1 type) STR ''max'' [Integer[?]]"
by eval
thus ?thesis by simp
qed

(*** Code *******************************************************************)

section ‹Code›

subsection ‹Positive Cases›

values "{(𝒟, τ). attribute Employee STR ''name'' 𝒟 τ}"
values "{(𝒟, end). association_end Employee None STR ''employees'' 𝒟 end}"
values "{(𝒟, end). association_end Employee (Some STR ''project_manager'') STR ''employees'' 𝒟 end}"
values "{op. operation Project[1] STR ''membersCount'' [] op}"
values "{op. operation Project[1] STR ''membersByName'' [String[1]] op}"
value "has_literal STR ''E1'' STR ''A''"

text ‹
▩‹context Employee:
projects.members : Bag(Employee[1])››
values
"{τ. Γ⇩0(STR ''self'' ↦⇩f Employee[1]) ⊢
AssociationEndCall (AssociationEndCall (Var STR ''self'')
DotCall None STR ''projects'')
DotCall None STR ''members'' : τ}"

subsection ‹Negative Cases›

values "{(𝒟, τ). attribute Employee STR ''name2'' 𝒟 τ}"
value "has_literal STR ''E1'' STR ''C''"

text ‹
▩‹Sequence{1..5, null}->max()››
values
"{τ. Γ⇩0 ⊢ OperationCall (CollectionLiteral SequenceKind
[CollectionRange (IntegerLiteral 1) (IntegerLiteral 5),
CollectionItem NullLiteral])
ArrowCall CollectionMaxOp [] : τ}"

end