Theory OCL_Examples

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
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)"
| "Task ⊔ c = (if c = Task then Task 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 (simp add: less_le_not_le_classes1)
  apply (simp add: order_refl_classes1)
  apply (rule order_trans_classes1; auto)
  apply (simp add: antisym_classes1)
  apply (simp add: sup_ge1_classes1)
  apply (simp add: sup_ge2_classes1)
  by (simp add: sup_least_classes1)

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[?])]),
  (Task, fmap_of_list [
    (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 ''ProjectTask'' ↦⇩f [
    STR ''project'' ↦⇩f (Project, 1, 1, False, False),
    STR ''tasks'' ↦⇩f (Task, 0, ∞, True, True)],
  STR ''SprintTaskAssignee'' ↦⇩f [
    STR ''sprint'' ↦⇩f (Sprint, 0, 10, False, True),
    STR ''tasks'' ↦⇩f (Task, 0, 5, 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