% everything graphical_bon: THEORY BEGIN IMPORTING ecore_fragment, bon_ecore_metamodel, bon_visual_model, bon_visual_class_model, bon_visual_static_diagram_model END graphical_bon % formalization of (fragment of) ECORE ecore_fragment: THEORY BEGIN % full type hierarchy of ecore from % http://www.monperrus.net/martin/the-class-diagram-of-the-ecore-metamodel.pdf EStringToStringMapEntry: TYPE EObject: TYPE EModelElement, EGenericType: TYPE FROM EObject EAnnotation, EFactory, ENamedElement: TYPE FROM EModelElement EClassifier, ETypedElement, ETypedParameter, EEnumLiteral, EPackage: TYPE FROM ENamedElement EClass, EDataType: TYPE FROM EClassifier EEnum: TYPE FROM EDataType EStructuralFeature, EParameter, EOperation: TYPE FROM ETypedElement EAttribute, EReference: TYPE FROM EStructuralFeature END ecore_fragment % formalization of (fragment of) BON ECORE metamodel bon_ecore_metamodel: THEORY BEGIN IMPORTING ecore_fragment % from BON_IDE/bonIDE/model/bonide.ecore % also https://mobius.ucd.ie/trac/browser/src/bon/BON_IDE/bonIDE/text/description.txt?format=txt Model, Abstraction: TYPE FROM EClass StaticAbstraction: TYPE FROM Abstraction Cluster: TYPE FROM StaticAbstraction BONClass: TYPE FROM StaticAbstraction static_abstraction_is_class_or_cluster: AXIOM (FORALL (sa:StaticAbstraction): BONClass_pred(sa) OR Cluster_pred(sa)) Feature, IndexClause, InheritanceClause, FeatureArgument: TYPE FROM EClass PreCondition, PostCondition, Invariant: TYPE FROM EClass StaticRelationship: TYPE FROM EClass InheritanceRel, ClientSupplierRel: TYPE FROM StaticRelationship AggregationRel, AssociationRel: TYPE FROM ClientSupplierRel % Inheritance, Aggregation, Association RelationshipType: TYPE FROM EEnum % Reused, Persistent, Deferred, Effective, Interfaced, Root, Parameterized ImplementationStatus: TYPE FROM EEnum system_cluster?: [Cluster -> bool] END bon_ecore_metamodel % formalization of (fragment of) graphical language of BON bon_visual_model: THEORY BEGIN IMPORTING bon_ecore_metamodel, digraphs@trees, digraphs@walks, digraphs@digraphs % we want to say that a legitimate inheritance relation defines % a tree on BONClasses rooted at a constant BONClass ANY ANY: BONClass inheritance_tree: TYPE = { t: Tree[BONClass] | root?(t)(ANY) } cluster_tree: TYPE = { t: Tree[StaticAbstraction] | EXISTS (c: Cluster): root?(t)(c) AND system_cluster?(c) AND FORALL (e: (edges(t))): Cluster_pred(e`1) } ancestor?(t: inheritance_tree, c, p: BONClass): bool = EXISTS (w: Walk[BONClass](t)): 2 <= l(w) AND w`seq(0) = p AND w`seq(l(w)-1) = c ANY_is_ancestor_to_all: LEMMA FORALL (t: inheritance_tree, c: {d: (vert(t)) | d /= ANY}): ancestor?(t, c, ANY) client_digraph: TYPE = digraph[BONClass] BON_model_rec: TYPE = [# inheritance_relations: inheritance_tree, clustering_relations: cluster_tree, client_relations: client_digraph #] c: VAR BONClass class_vert(ct:cluster_tree)(c): bool = vert(ct)(c) BON_model?(m:BON_model_rec): bool = vert(m`inheritance_relations) = class_vert(m`clustering_relations) AND subset?(vert(m`client_relations), vert(m`inheritance_relations)) BON_model: TYPE = (BON_model?) RelType: TYPE = {AGGREGATION, ASSOCIATION, SHARED} ClientDigraphLabel: TYPE cdl: VAR ClientDigraphLabel label_type(cdl): RelType client_label(bm:BON_model)(edge:(edges(bm`client_relations))): ClientDigraphLabel multiplicity(cdl): int END bon_visual_model % formalize what a class looks like in a visual diagram bon_visual_class_model: THEORY BEGIN IMPORTING bon_ecore_metamodel C: VAR Cluster K: VAR BONClass SR: VAR StaticRelationship F: VAR Feature IC: VAR bon_ecore_metamodel.IndexClause I: VAR Invariant S: VAR string abstractions: [Model -> Abstraction] relationships: [Model -> StaticRelationship] contents?(C)(SR): bool cluster_name: [Cluster -> string] collapsed: [Cluster -> bool] expandedHeight: [Cluster -> int] class_name: [BONClass -> string] features?(K)(F): bool isDeferred?: [BONClass -> bool] implementationStatus: [BONClass -> ImplementationStatus] indexes?(K)(IC): bool parents: [BONClass -> InheritanceClause] invariants?(K)(I): bool names?(F)(S): bool % ... END bon_visual_class_model % formalize what a visualization of a static diagram looks like bon_visual_static_diagram_model: THEORY BEGIN IMPORTING bon_visual_model %TODO these do not have to be trees, just digraphs BON_model_view_rec: TYPE = [# inheritance_relations: lift[inheritance_tree], clustering_relations: lift[cluster_tree], client_relations: client_digraph #] BON_model_view?(m: BON_model)(v: BON_model_view_rec): bool = CASES v`inheritance_relations OF bottom: true, up(ig): di_subgraph?(ig, m`inheritance_relations) ENDCASES AND CASES v`clustering_relations OF bottom: true, up(cg): di_subgraph?(cg, m`clustering_relations) ENDCASES AND di_subgraph?(v`client_relations, m`client_relations) view: TYPE = [ m: BON_model -> (BON_model_view?(m)) ] END bon_visual_static_diagram_model viz_to_typesystem: THEORY BEGIN IMPORTING graphical_bon IMPORTING type_context bc: VAR BONClass bm, bm1, bm2: VAR BON_model ftc: VAR Formal_TC cl: VAR Cluster fcd: VAR FormalClassDefinition %All the classes in a BON_model all_classes(bm): finite_set[BONClass] = bm`inheritance_relations`vert %All the clusters in a BON_model all_clusters(bm): finite_set[Cluster] = { c: Cluster | vert(bm`clustering_relations)(c) } %Convert a BON_model class to a FormalClassDefinition bm_class_to_tc_class(bc): FormalClassDefinition bm_class_to_tc_class_is_bijective: AXIOM bijective?(bm_class_to_tc_class) %Convert a BON_model cluster to a FormalClusterDefinition bm_cluster_to_tc_cluster(cl): FormalClusterDefinition bm_cluster_to_tc_cluster_is_bijective: AXIOM bijective?(bm_cluster_to_tc_cluster) %Convert a BON_model static abstraction (class or cluster) to a FormalBonType bm_abs_to_tc_type(abs:StaticAbstraction): FormalBonType bm_abs_to_tc_type_is_bijective: AXIOM bijective?(bm_abs_to_tc_type) %Convert a (finite) set of BONClasses to a set of FormalClassDefinitions bm_classes_to_tc_classes(s:finite_set[BONClass]): finite_set[FormalClassDefinition] = % { r: finite_set[FormalClassDefinition] | % (FORALL (c: BONClass): member(c, s) => member(bm_class_to_tc_class(c), r)) AND % (FORALL (d: FormalClassDefinition): member(d, r) => % (EXISTS (c: BONClass): member(c,s) AND bm_class_to_tc_class(c)=d)) } % { fcd | (EXISTS bc: s(bc) AND bm_class_to_tc_class(bc) = fcd) } {fcd | some((LAMBDA bc: bm_class_to_tc_class(bc)=fcd))(s)} bm_classes_to_tc_classes_finite: LEMMA (FORALL (s:finite_set[BONClass]): is_finite(bm_classes_to_tc_classes(s))) %Proved bm_classes_to_tc_classes_card: LEMMA (FORALL (s:finite_set[BONClass]): card(s) = card(bm_classes_to_tc_classes(s))) %Not proved bm_classes_to_tc_classes_bijective: LEMMA bijective?(bm_classes_to_tc_classes) %Not proved bm_classes_to_tc_classes_map(s:set[BONClass]): Formal_TC_Classes = build_map[FormalClassType,FormalClassDefinition](formal_class_definition_to_formal_class_type)(bm_classes_to_tc_classes(s)) bm_classes_to_tc_classes_map_bijective: LEMMA bijective?(bm_classes_to_tc_classes_map) bm_clusters_to_tc_clusters(s:finite_set[Cluster]): finite_set[FormalClusterDefinition] = { fcd:FormalClusterDefinition | (EXISTS (bc:(s)): bm_cluster_to_tc_cluster(bc)=fcd) } bm_clusters_to_tc_clusters_map(s:finite_set[Cluster]): Formal_TC_Clusters = build_map[FormalClusterType,FormalClusterDefinition](formal_cluster_definition_to_formal_cluster_type)(bm_clusters_to_tc_clusters(s)) bm_clusters_to_tc_clusters_map_bijective: LEMMA bijective?(bm_clusters_to_tc_clusters_map) %TODO client entities bm_client_to_tc_rel(bm:BON_model)(x,y:Abstraction): TypeRelationPair = LET label:ClientDigraphLabel=client_label(bm)(x,y), rel_type:RelType=label_type(label), source:BonType=bm_abs_to_tc_type(x), target:BonType=bm_abs_to_tc_type(y) IN CASES rel_type OF AGGREGATION: client_relation(source, target, aggregate), ASSOCIATION: client_relation(source, target, has), SHARED: client_relation(source, target, shared(multiplicity(label))) ENDCASES bm_clients_to_tc_rels(bm): set[TypeRelationPair] = LET clustering_edges:finite_set[[Abstraction,Abstraction]]=edges(bm`clustering_relations) IN { trp:TypeRelationPair | (EXISTS (edge:(clustering_edges)): bm_client_to_tc_rel(bm)(edge)=trp) } bm_clients_to_tc_rels_bijective: LEMMA bijective?(bm_clients_to_tc_rels) %Our overall translation from graphical to textual graph_to_text_translation(bm): Formal_TC = (# level:=FORMAL_LEVEL, classes:=bm_classes_to_tc_classes_map(all_classes(bm)), clusters:=bm_clusters_to_tc_clusters_map(all_clusters(bm)), system:=formal_cluster_definition_to_formal_cluster_type(bm_cluster_to_tc_cluster(root?(bm`clustering_relations))), relations:=bm_clients_to_tc_rels(bm) #) %text_to_graph_translation: [Formal_TC -> BON_model] %inverse_translation: AXIOM inverse?(text_to_graph_translation)(graph_to_text_translation) %inverse_translation2: AXIOM inverse?(graph_to_text_translation)(text_to_graph_translation) %inverse_translation_lem_1: LEMMA graph_to_text_translation(text_to_graph_translation(ftc)) = ftc %inverse_translation_lem_2: LEMMA text_to_graph_translation(graph_to_text_translation(bm)) = bm %TODO - this is the real meat of what we need to prove injective_translation: LEMMA injective?(graph_to_text_translation) surjective_translation: LEMMA surjective?(graph_to_text_translation) bijective_translation: LEMMA bijective?(graph_to_text_translation) %The equivalence relation over BON_model and Formal_TC text_graph_equivalence_relation: pred[[BON_model,Formal_TC]] = graph(graph_to_text_translation) equivalence_is_isomorphic: LEMMA isomorphism?(text_graph_equivalence_relation) END viz_to_typesystem graph_diffing[T: TYPE]: THEORY BEGIN IMPORTING digraphs@digraphs g1, g2: VAR digraph[T] difference(g1, g2): digraph[T] = (# vert:=difference(vert(g1),vert(g2)), edges:=difference(edges(g1),edges(g2)) #) merge(g1, g2): digraph[T] = union(g1,g2) %(# vert:=union(vert(g1),vert(g2)), edges:=union(edges(g1),edges(g2)) #) diff_union_graph: LEMMA union(difference(g1,g2),g2) = union(g1,g2) %Not proved, but should follow from union_difference in prelude END graph_diffing model_diffing: THEORY BEGIN IMPORTING graphical_bon, graph_diffing[BONClass], graph_diffing[StaticAbstraction] clustring_relations_diff_graph: TYPE = { d: digraph[StaticAbstraction] | FORALL (e: (edges(d))): Cluster_pred(e`1) } ModelDiffEl: TYPE = [# ir: digraph[BONClass], cr: digraph[StaticAbstraction], clr: digraph[BONClass] #] ModelDiff: TYPE = [# add:ModelDiffEl, remove:ModelDiffEl #] bm1,bm2: VAR BON_model difference(bm1,bm2): ModelDiffEl = (# ir:=difference(inheritance_relations(bm1),inheritance_relations(bm2)), cr:=difference(clustering_relations(bm1),clustering_relations(bm2)), clr:=difference(client_relations(bm1),client_relations(bm2)) #) compute_diff(bm1,bm2): ModelDiff = (# add:=difference(bm2,bm1), remove:=difference(bm1,bm2) #) d: VAR ModelDiff apply_diff(d,bm1): BON_model = (# inheritance_relations:= difference(merge(inheritance_relations(bm1),ir(d`add)),ir(d`remove)), clustering_relations:= difference(merge(clustering_relations(bm1),cr(d`add)),cr(d`remove)), client_relations:= difference(merge(client_relations(bm1),clr(d`add)),clr(d`remove)) #) x: LEMMA apply_diff(compute_diff(bm1,bm2),bm1) = bm2 %Not proved %TODO diff on textual side %TODO translate diff END model_diffing