Theory OCL_Object_Model
chapter ‹Object Model›
theory OCL_Object_Model
imports OCL_Syntax
begin
text ‹
I see no reason why objects should refer nulls using multi-valued
associations. Therefore, multi-valued associations have collection
types with non-nullable element types.›
definition
"assoc_end_type end ≡
let 𝒞 = assoc_end_class end in
if assoc_end_max end ≤ (1 :: nat) then
if assoc_end_min end = (0 :: nat)
then ⟨𝒞⟩⇩𝒯[?]
else ⟨𝒞⟩⇩𝒯[1]
else
if assoc_end_unique end then
if assoc_end_ordered end
then OrderedSet ⟨𝒞⟩⇩𝒯[1]
else Set ⟨𝒞⟩⇩𝒯[1]
else
if assoc_end_ordered end
then Sequence ⟨𝒞⟩⇩𝒯[1]
else Bag ⟨𝒞⟩⇩𝒯[1]"
definition "class_assoc_type 𝒜 ≡ Set ⟨𝒜⟩⇩𝒯[1]"
definition "class_assoc_end_type end ≡ ⟨assoc_end_class end⟩⇩𝒯[1]"
definition "oper_type op ≡
let params = oper_out_params op in
if length params = 0
then oper_result op
else Tuple (fmap_of_list (map (λp. (param_name p, param_type p))
(params @ [(STR ''result'', oper_result op, Out)])))"
class ocl_object_model =
fixes classes :: "'a :: semilattice_sup fset"
and attributes :: "'a ⇀⇩f attr ⇀⇩f 'a type"
and associations :: "assoc ⇀⇩f role ⇀⇩f 'a assoc_end"
and association_classes :: "'a ⇀⇩f assoc"
and operations :: "('a type, 'a expr) oper_spec list"
and literals :: "'a enum ⇀⇩f elit fset"
assumes assoc_end_min_less_eq_max:
"assoc |∈| fmdom associations ⟹
fmlookup associations assoc = Some ends ⟹
role |∈| fmdom ends ⟹
fmlookup ends role = Some end ⟹
assoc_end_min end ≤ assoc_end_max end"
assumes association_ends_unique:
"association_ends' classes associations 𝒞 from role end⇩1 ⟹
association_ends' classes associations 𝒞 from role end⇩2 ⟹ end⇩1 = end⇩2"
begin
interpretation base: object_model
by standard (simp_all add: local.assoc_end_min_less_eq_max local.association_ends_unique)
abbreviation "owned_attribute ≡ base.owned_attribute"
abbreviation "attribute ≡ base.attribute"
abbreviation "association_ends ≡ base.association_ends"
abbreviation "owned_association_end ≡ base.owned_association_end"
abbreviation "association_end ≡ base.association_end"
abbreviation "referred_by_association_class ≡ base.referred_by_association_class"
abbreviation "association_class_end ≡ base.association_class_end"
abbreviation "operation ≡ base.operation"
abbreviation "operation_defined ≡ base.operation_defined"
abbreviation "static_operation ≡ base.static_operation"
abbreviation "static_operation_defined ≡ base.static_operation_defined"
abbreviation "has_literal ≡ base.has_literal"
lemmas attribute_det = base.attribute_det
lemmas attribute_self_or_inherited = base.attribute_self_or_inherited
lemmas attribute_closest = base.attribute_closest
lemmas association_end_det = base.association_end_det
lemmas association_end_self_or_inherited = base.association_end_self_or_inherited
lemmas association_end_closest = base.association_end_closest
lemmas association_class_end_det = base.association_class_end_det
lemmas operation_det = base.operation_det
lemmas static_operation_det = base.static_operation_det
end
end