Quelle  OCL_Examples.thy

(*  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 C = False"
| "subclass1_fun Person C = (C = Object)"
| "subclass1_fun Employee C = (C = Object ∨ C = Person)"
| "subclass1_fun Customer C = (C = Object ∨ C = Person)"
| "subclass1_fun Project C = (C = Object)"
| "subclass1_fun Task C = (C = Object)"
| "subclass1_fun Sprint C = (C = Object)"

lemma less_classes1_code [code]:
  "(<) = subclass1_fun"
proof (intro ext iffI)
  fix C D :: "classes1"
  show "C < D ==> subclass1_fun C D"
    unfolding less_classes1_def
    apply (erule subclass1.cases, auto)
    using subclass1_fun.elims(3) by blast
  show "subclass1_fun C D ==> C < D"
    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 "Γ₀ ≡ 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}
  Project
 : membersCount() : Integer[1] = members->size()
 : membersByName(mn : String[1]) : Set(Employee[1]) =
 members->select(member | member.name = mn)
  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 C from role end₁"
      and "association_ends' classes assocs C from role end₂"
    shows "end₁ = end₂"
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'' D τ =
   (D = 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'' D τ =
   (D = 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'' D τ =
   (D = 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⟩_\<T>[1] STR ''allProjects'' [] oper =
   (oper = (STR ''allProjects'', ⟨Project⟩_\<T>[1], [], Set ⟨Project⟩_\<T>[1], True,
     Some (MetaOperationCall ⟨Project⟩_\<T>[1] AllInstancesOp)))"
proof -
  have "static_operation ⟨Project⟩_\<T>[1] STR ''allProjects'' []
    (STR ''allProjects'', ⟨Project⟩_\<T>[1], [], Set ⟨Project⟩_\<T>[1], True,
     Some (MetaOperationCall ⟨Project⟩_\<T>[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⟩_\<T> < ⟨Person⟩_\<T>" by auto
lemma "⟨Person⟩_\<T> ≤ 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
  "Γ₀ ⊨ EnumLiteral STR ''E1'' STR ''A'' : (Enum STR ''E1'')[1]"
  by simp

text ‹
 🍋‹true or false : Boolean[1]››
lemma
  "Γ₀ ⊨ OperationCall (BooleanLiteral True) DotCall OrOp
    [BooleanLiteral False] : Boolean[1]"
  by simp

text ‹
 🍋‹null and true : Boolean[?]››
lemma
  "Γ₀ ⊨ OperationCall (NullLiteral) DotCall AndOp
    [BooleanLiteral True] : Boolean[?]"
  by simp

text ‹
 🍋‹let x : Real[1] = 5 in x + 7 : Real[1]››
lemma
  "Γ₀ ⊨ 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
  "Γ₀ ⊨ OperationCall (NullLiteral) DotCall OclIsUndefinedOp [] : Boolean[1]"
  by simp

text ‹
 🍋‹Sequence{1..5, null}.oclIsUndefined() : Sequence(Boolean[1])››
lemma
  "Γ₀ ⊨ 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
  "Γ₀ ⊨ 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
  "Γ₀ ⊨ 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
  "Γ₀ ⊨ 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
 ->any(it | it = 'test') : String[?]››
lemma
  "Γ₀ ⊨ 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
 ?->closure(it | it) : OrderedSet(String[1])››
lemma
  "Γ₀ ⊨ 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:
  : String[1]››
lemma
  "Γ₀(STR ''self'' ↦_f Employee[1]) ⊨
    AttributeCall (Var STR ''self'') DotCall STR ''name'' : String[1]"
  by simp

text ‹
 🍋‹context Employee:
  : Set(Project[1])››
lemma
  "Γ₀(STR ''self'' ↦_f Employee[1]) ⊨
    AssociationEndCall (Var STR ''self'') DotCall None
      STR ''projects'' : Set Project[1]"
  by simp

text ‹
 🍋‹context Employee:
 .members : Bag(Employee[1])››
lemma
  "Γ₀(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
  "Γ₀ ⊨ MetaOperationCall Project[?] AllInstancesOp : Set Project[?]"
  by simp

text ‹
 🍋‹Project[1]::allProjects() : Set(Project[1])››
lemma
  "Γ₀ ⊨ StaticOperationCall Project[1] STR ''allProjects'' [] : Set Project[1]"
  by simp

subsection ‹Negative Cases›

text ‹
 🍋‹true = null››
lemma
  "∄τ. Γ₀ ⊨ OperationCall (BooleanLiteral True) DotCall EqualOp
    [NullLiteral] : τ"
  by simp

text ‹
 🍋‹let x : Boolean[1] = 5 in x and true››
lemma
  "∄τ. Γ₀ ⊨ 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
 ->closure(it | 1)››
lemma
  "∄τ. Γ₀ ⊨ 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
  "∄τ. Γ₀ ⊨ 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 "{(D, τ). attribute Employee STR ''name'' D τ}"
values "{(D, end). association_end Employee None STR ''employees'' D end}"
values "{(D, end). association_end Employee (Some STR ''project_manager'') STR ''employees'' D 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:
 .members : Bag(Employee[1])››
values
  "{τ. Γ₀(STR ''self'' ↦_f Employee[1]) ⊨
    AssociationEndCall (AssociationEndCall (Var STR ''self'')
        DotCall None STR ''projects'')
      DotCall None STR ''members'' : τ}"

subsection ‹Negative Cases›

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

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

end