diff --git a/su4sml/src/wfcpog/interface_consistency.sml b/su4sml/src/wfcpog/interface_consistency.sml index e9af7bd..a99f858 100644 --- a/su4sml/src/wfcpog/interface_consistency.sml +++ b/su4sml/src/wfcpog/interface_consistency.sml @@ -42,9 +42,16 @@ (** Implementation of the Liskov Substitiution Principle. *) signature WFCPOG_INTERFACE_CONSTRAINT = sig - val has_consistent_stereotypes : WFCPOG.wfpo -> Rep.Model -> bool - - val is_nameclash_free : WFCPOG.wfpo -> Rep.Model -> bool + (** + * Checks if the operations of the interface do not have the + * stereotypyes 'create' or 'destroy'. + *) + val check_stereotypes : WFCPOG.wfpo -> Rep.Model -> bool + (** + * Checks that a classifier implementing more then one interface + * has no nameclashes. + *) + val check_nameclashes : WFCPOG.wfpo -> Rep.Model -> bool end structure WFCPOG_Interface_Constraint:WFCPOG_INTERFACE_CONSTRAINT = struct @@ -72,48 +79,112 @@ fun list_has_dup [] = false else list_has_dup (tail) -fun has_consistent_stereotypes_help [] model = true - | has_consistent_stereotypes_help ((Interface{operations,...})::classes) (model as (clist,alist)) = - List.all (fn a => not (List.exists (fn b => (b = "create") orelse (b = "destroy")) (#stereotypes a))) (operations) - | has_consistent_stereotypes_help (h::classes) model = has_consistent_stereotypes_help classes model +fun check_stereotypes_interface (i as Interface{operations,...}) (model as (clist,alist)) = + if (List.all (fn a => not (List.exists (fn b => (b = "create") orelse (b = "destroy")) (#stereotypes a))) (operations)) + then true + else + let + val s1 = "SYNTAX ERROR: Interface stereotypes consistency\n\n" + val s2 = "Interface " ^ (string_of_path (name_of i)) ^ " has a operations with stereotypes 'create' or 'destroy' \n" + in + raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + end + | check_stereotypes_interface x model = true -fun is_nameclash_free_help [] model = true - | is_nameclash_free_help ((Class{interfaces,...})::classes) (model as (clist,alist)) = + +fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,alist)) = if (List.length(interfaces)) <= 1 - then is_nameclash_free_help classes model + then true else let val if_list = List.map (fn a => class_of_type a model) interfaces val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of a model))) if_list) in - list_has_dup (op_name_list) + if (not (list_has_dup (op_name_list))) + then true + else + let + val s1 = "SYNTAX ERROR: Interface nameclash consistency\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of c)) ^ " has a nameclash resulting from the interfaces " ^ (String.concat (List.map (fn a => (string_of_OclType a)) interfaces)) ^ ".\n" + in + raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + end end - | is_nameclash_free_help ((AssociationClass{interfaces,...})::classes) (model as (clist,alist)) = - if (List.length(interfaces)) <= 1 - then is_nameclash_free_help classes model + | check_nameclash_classifier (a as AssociationClass{interfaces,...}) (model as (clist,alist)) = + if (List.length(interfaces)) <= 1 + then true else let val if_list = List.map (fn a => class_of_type a model) interfaces val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of a model))) if_list) in - list_has_dup (op_name_list) + if (not (list_has_dup (op_name_list))) + then true + else + let + val s1 = "SYNTAX ERROR: Interface nameclash consistency\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of a)) ^ " has a nameclash resulting from the interfaces " ^ (String.concat (List.map (fn a => (string_of_OclType a)) interfaces)) ^ ".\n" + in + raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + end end - | is_nameclash_free_help (x::classes) model = is_nameclash_free_help classes model + | check_nameclash_classifier (e as Enumeration{interfaces,...}) model = + if (List.length(interfaces)) <= 1 + then true + else + let + val if_list = List.map (fn a => class_of_type a model) interfaces + val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of a model))) if_list) + in + if (not (list_has_dup (op_name_list))) + then true + else + let + val s1 = "SYNTAX ERROR: Interface nameclash consistency\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of e)) ^ " has a nameclash resulting from the interfaces " ^ (String.concat (List.map (fn a => (string_of_OclType a)) interfaces)) ^ ".\n" + in + raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + end + end + | check_nameclash_classifier (p as Primitive{interfaces,...}) model = + if (List.length(interfaces)) <= 1 + then true + else + let + val if_list = List.map (fn a => class_of_type a model) interfaces + val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of a model))) if_list) + in + if (not (list_has_dup (op_name_list))) + then true + else + let + val s1 = "SYNTAX ERROR: Interface nameclash consistency\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of p)) ^ " has a nameclash resulting from the interfaces " ^ (String.concat (List.map (fn a => string_of_OclType a) interfaces)) ^ ".\n" + in + raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + end + end + | check_nameclash_classifier x model = true - -fun has_consistent_stereotypes wfpo (model as (clist,alist)) = +fun check_stereotypes wfpo (model as (clist,alist)) = let - val classes = removeOclLibrary clist + val _ = trace function_calls ("WFCPOG_Interface_Consistency.check_stereotypes\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Iface a)) cl + val res = List.all (fn a => a = true) (List.map (fn a => check_stereotypes_interface a model) classes) + val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_stereotypes\n") in - has_consistent_stereotypes_help classes model + res end -fun is_nameclash_free wfpo (model as (clist,alist)) = +fun check_nameclashes wfpo (model as (clist,alist)) = let - val classes = removeOclLibrary clist + val _ = trace function_calls ("WFCPOG_Interface_Consistency.check_nameclashes\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a) orelse (is_Primi a) orelse (is_Enum a)) cl + val res = List.all (fn a => a = true) (List.map (fn a => check_nameclash_classifier a model) classes) + val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_nameclashes\n") in - is_nameclash_free_help classes model + res end - - end; diff --git a/su4sml/src/wfcpog/load_model.sml b/su4sml/src/wfcpog/load_model.sml index cbb6340..a6ca91e 100644 --- a/su4sml/src/wfcpog/load_model.sml +++ b/su4sml/src/wfcpog/load_model.sml @@ -16,7 +16,7 @@ val prefix = "../../../hol-ocl/examples/" val _ = Control.Print.printDepth:=20 val _ = Control.Print.printLength:=30 -(* +(* val zargo = prefix^"simple_rfm/simple_rfm.zargo" val ocl = prefix^"simple_rfm/simple_rfm.ocl" val remP = [] @@ -40,11 +40,11 @@ val remP = [] (** OVERRIDING **) - +(* val zargo = "../../../hol-ocl/examples/overriding/overriding.zargo" val ocl="../../../hol-ocl/examples/overriding/overriding.ocl" val remP = [] - +*) (** ISP **) (* @@ -86,11 +86,11 @@ val zargo = "../../../hol-ocl/examples/overriding/overriding.zargo" val ocl="../../../hol-ocl/examples/overriding/overriding.ocl" val remP = [] *) -(* + val zargo = "../../../hol-ocl/examples/stack_manu/stack.zargo" val ocl="../../../hol-ocl/examples/stack_manu/stack.ocl" val remP = [] -*) + (** import model *) val XMI = parseUML zargo val _ = init_offset() diff --git a/su4sml/src/wfcpog/test-data.sml b/su4sml/src/wfcpog/test-data.sml index 81db050..07e9eae 100644 --- a/su4sml/src/wfcpog/test-data.sml +++ b/su4sml/src/wfcpog/test-data.sml @@ -18,7 +18,9 @@ val _ = trace wgen "\n\n\n" (** ################# **) (** INTERFACE CONSTRAINT **) -val wfc_inf = get_wfpo supported_wfs "wfc_inf" +val wfc_inf_nameclashes = get_wfpo supported_wfs "wfc_inf_nameclashes" +val wfc_inf_stereotypes = get_wfpo supported_wfs "wfc_inf_stereotypes" +val wfc_inf_all = get_wfpo supported_wfs "wfc_inf_all" val _ = trace high ("............. interface constraint loaded ...\n") (** VISIBILITY CONSTRAINT **) diff --git a/su4sml/src/wfcpog/wfcpog_registry.sml b/su4sml/src/wfcpog/wfcpog_registry.sml index 2d40d74..f9003f0 100644 --- a/su4sml/src/wfcpog/wfcpog_registry.sml +++ b/su4sml/src/wfcpog/wfcpog_registry.sml @@ -168,33 +168,33 @@ val tax_workaround = val supported_wfs = [ WFCPOG.WFPO{ - identifier = "wfc_inf_ster", + identifier = "wfc_inf_stereotypes", name = "WFC Interface Consistency consistent stereotypes (subconstraint)", description = "Checks if all operations of an interface don't have the stereotypes 'create' or 'destroy'.\n", recommended = false, depends = [], recommends = [], - apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.has_consistent_stereotypes), + apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.check_stereotypes), data = Datatab.empty }, WFCPOG.WFPO{ - identifier = "wfc_inf_name", + identifier = "wfc_inf_nameclashes", name = "WFC Interface Consistency no nameclashes (subconstraint)", description = "Checks for classes inheriting from more than one interface that there are no nameclashes.\n", recommended = false, depends = [], recommends = [], - apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.is_nameclash_free), + apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.check_nameclashes), data = Datatab.empty }, WFCPOG.WFPO{ - identifier = "wfc_inf", + identifier = "wfc_inf_all", name = "WFC Interface Consistency (complete)", description = "Checking of two subconstraints: \n wfc_inf_ster: Checks if all operations of an interface don't have the stereotypes 'create' or 'destroy'. \n wfc_inf_name : Checks for classes inheriting from more than one interface that there are no nameclashes.\n", recommended = true, - depends = ["wfc_inf_ster"], + depends = ["wfc_inf_stereotypes"], recommends = [], - apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.is_nameclash_free), + apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.check_nameclashes), data = Datatab.empty }, WFCPOG.WFPO{