From 7e35a497fc72303c9a35d2db647d65c2dfa316d8 Mon Sep 17 00:00:00 2001 From: Manuel Krucker Date: Fri, 9 May 2008 00:19:36 +0000 Subject: [PATCH] new exception added git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7924 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/wfcpog/constructor_consistency.sml | 3 +- su4sml/src/wfcpog/interface_consistency.sml | 12 ++++--- su4sml/src/wfcpog/load_model.sml | 8 ++--- su4sml/src/wfcpog/refine_constraint.sml | 11 ++++--- su4sml/src/wfcpog/taxonomy_consistency.sml | 3 +- su4sml/src/wfcpog/test-data.sml | 10 ++++-- su4sml/src/wfcpog/test-suite.sml | 31 +++++++++++-------- su4sml/src/wfcpog/visibility_consistency.sml | 16 ++++++---- su4sml/src/wfcpog/wfcpog.sml | 7 +++-- 9 files changed, 62 insertions(+), 39 deletions(-) diff --git a/su4sml/src/wfcpog/constructor_consistency.sml b/su4sml/src/wfcpog/constructor_consistency.sml index 30d7046..d915c5a 100644 --- a/su4sml/src/wfcpog/constructor_consistency.sml +++ b/su4sml/src/wfcpog/constructor_consistency.sml @@ -103,7 +103,7 @@ fun check_override_classifier class (model as (clist,alist)) = val s1 = "SYNTAX ERROR: Constructor Consistency override old creators\n\n" val s2 = "In the classifier " ^ (string_of_path (name_of class)) ^ " the Creator " ^ (name_of_op a) ^ "is not overriden.\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end) creas val res = List.all (fn a => a = true) check val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") @@ -154,6 +154,7 @@ fun override_old_creators wfpo (model as (clist, alist)) = val _ = trace function_calls ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) end fun post_implies_invariant wfpo (model as (clist, alist)) = diff --git a/su4sml/src/wfcpog/interface_consistency.sml b/su4sml/src/wfcpog/interface_consistency.sml index a99f858..ea68bdc 100644 --- a/su4sml/src/wfcpog/interface_consistency.sml +++ b/su4sml/src/wfcpog/interface_consistency.sml @@ -87,7 +87,7 @@ fun check_stereotypes_interface (i as Interface{operations,...}) (model as (clis 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) + raise WFCPOG.WFC_FailedMessage (s1^s2) end | check_stereotypes_interface x model = true @@ -107,7 +107,7 @@ fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,ali 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) + raise WFCPOG.WFC_FailedMessage (s1^s2) end end | check_nameclash_classifier (a as AssociationClass{interfaces,...}) (model as (clist,alist)) = @@ -125,7 +125,7 @@ fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,ali 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) + raise WFCPOG.WFC_FailedMessage (s1^s2) end end | check_nameclash_classifier (e as Enumeration{interfaces,...}) model = @@ -143,7 +143,7 @@ fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,ali 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) + raise WFCPOG.WFC_FailedMessage (s1^s2) end end | check_nameclash_classifier (p as Primitive{interfaces,...}) model = @@ -161,7 +161,7 @@ fun check_nameclash_classifier (c as Class{interfaces,...}) (model as (clist,ali 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) + raise WFCPOG.WFC_FailedMessage (s1^s2) end end | check_nameclash_classifier x model = true @@ -175,6 +175,7 @@ fun check_stereotypes wfpo (model as (clist,alist)) = val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_stereotypes\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) end fun check_nameclashes wfpo (model as (clist,alist)) = @@ -186,5 +187,6 @@ fun check_nameclashes wfpo (model as (clist,alist)) = val _ = trace function_ends ("WFCPOG_Interface_Consistency.check_nameclashes\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) end end; diff --git a/su4sml/src/wfcpog/load_model.sml b/su4sml/src/wfcpog/load_model.sml index a6ca91e..c03c2f3 100644 --- a/su4sml/src/wfcpog/load_model.sml +++ b/su4sml/src/wfcpog/load_model.sml @@ -25,11 +25,11 @@ val remP = [] val zargo = "../../../../examples/meeting/Meeting.zargo" val ocl = "" *) -(* + val zargo = "../../../hol-ocl/examples/SimpleChair/SimpleChair.zargo" val ocl = "../../../hol-ocl/examples/SimpleChair/AbstractSimpleChair04.ocl" val remP = ["AbstractSimpleChair02", "AbstractSimpleChair03","AbstractSimpleChair01","ConcreteSimpleChair01"] ; -*) + (** EBANK **) (* @@ -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/refine_constraint.sml b/su4sml/src/wfcpog/refine_constraint.sml index 4a6ffb8..97931b4 100644 --- a/su4sml/src/wfcpog/refine_constraint.sml +++ b/su4sml/src/wfcpog/refine_constraint.sml @@ -157,7 +157,7 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) = val s2 = ("The following public classes are not included in the refined class:\n\n") val s3 = (String.concat (List.map (fn a => (" * " ^ (string_of_path (name_of a)) ^ "\n")) clist)) in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3) end val _ = trace function_calls ("WFCPOG_Refine_Constraint.map_public_classes\n") in @@ -182,7 +182,7 @@ fun map_public_ops [] = [[]] val s4 = ("The following public operations are not included in the refined classes:\n\n") val s5 = (String.concat (List.map (fn a => (" * " ^ (operation2string a) ^ "\n")) oplist)) in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4^s5) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4^s5) end ))] @(map_public_ops tail) @@ -224,7 +224,7 @@ fun map_types [] fP tP model = [] val s5 = ("Existing FromClass = " ^ (string_of_path (name_of h1)) ^ "\n") val s6 = ("Inexisting ToClass = " ^ (string_of_path (name_of h2)) ^ "\n") in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4^s5^s6) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4^s5^s6) end (* name of the arguments *) val _ = trace wgen ("map_types_6: " ^ string_of_path (name_of c1) ^ "\n") @@ -245,7 +245,7 @@ fun map_types [] fP tP model = [] val s6 = ("Existing FromClass = " ^ (string_of_path (name_of h1)) ^ "\n") val s7 = ("Inexisting ToClass = " ^ (string_of_path (name_of h2)) ^ "\n") in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4^s5^s6^s7) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4^s5^s6^s7) end end ) arg_class_name1 @@ -293,11 +293,12 @@ fun check_syntax wfpo (model:Rep.Model as (clist,alist)) = val s3 = ("SYNTAX ERROR: check_syntax\n\n") val s4 = ("No classifier where found with the package name of the abstract or concrete path.\n") in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4) end val _ = trace function_ends ("WFCPOG_Refine_Constraint.check_syntax\n") in check + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) end fun get_holocl_operation var_name oper class model = diff --git a/su4sml/src/wfcpog/taxonomy_consistency.sml b/su4sml/src/wfcpog/taxonomy_consistency.sml index bb3b30c..44f71f1 100644 --- a/su4sml/src/wfcpog/taxonomy_consistency.sml +++ b/su4sml/src/wfcpog/taxonomy_consistency.sml @@ -131,7 +131,7 @@ fun check_depth_classifier depth class (model as (clist,alist)) = val s1 = "SYNTAX ERROR: Taxonomy design consistency\n\n" val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has depth " ^ (Int.toString (d)) ^ ".\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end in check @@ -148,5 +148,6 @@ fun check_depth wfpo (model as (clist,alist)) = val _ = trace function_calls ("WFCPG_Taxonomy_Consistency.check_maxDepth\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfpo,s) end end; diff --git a/su4sml/src/wfcpog/test-data.sml b/su4sml/src/wfcpog/test-data.sml index 07939dc..37acccb 100644 --- a/su4sml/src/wfcpog/test-data.sml +++ b/su4sml/src/wfcpog/test-data.sml @@ -68,8 +68,8 @@ val po_om = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "po_oper_model" val _ = trace high ("............. operational constraint loaded ...\n") (** CONSTRUCTOR CONSTRAINT **) -val po_cstr = get_wfpo supported_pos "po_cstr_post" -val po_cstr = get_wfpo supported_pos "po_cstr_attribute" +val po_cstr_post = get_wfpo supported_pos "po_cstr_post" +val po_cstr_attribute = get_wfpo supported_pos "po_cstr_attribute" val po_cstr = get_wfpo supported_pos "po_cstr" val _ = trace high ("............. constructor constraints loaded ...\n") @@ -122,5 +122,11 @@ val pos = [po_cstr] val wfs = [wfc_vis] val pos = [] *) +(* val wfs = [] val pos = [po_rfm_SR] +*) +val wfc = +[wfc_inf_nameclashes,wfc_inf_stereotypes,wfc_inf_all,wfc_vis_class,wfc_vis_inheritance,wfc_vis_runtime,wfc_vis_design_by_contract,wfc_vis,wfc_tax] +val pos = +[po_lsk_pre,po_lsk_post,po_lsk_inv,po_cm,po_sm,po_om,po_cstr_post,po_cstr_attribute,po_cstr] diff --git a/su4sml/src/wfcpog/test-suite.sml b/su4sml/src/wfcpog/test-suite.sml index 7448754..20e7848 100644 --- a/su4sml/src/wfcpog/test-suite.sml +++ b/su4sml/src/wfcpog/test-suite.sml @@ -156,12 +156,12 @@ fun start_tests model [] = [] let val _ = trace wgen ("Testing a wellformed constraint: \n") val res_wfcs = check_wfcs model [h] - handle WFCPOG.WFCPOG_WFC_FailedException s => + handle WFCPOG.WFC_FailedMessage s => let val _ = trace wgen ("WFC_Failed_Exception handler ...\n") val _ = buffer:=((!buffer)^s) in - [false] + [(h,false)] end val check = List.all (fn (a,b) => b = true) res_wfcs in @@ -187,33 +187,38 @@ fun start_tests model [] = [] in ([])@(start_tests model wfpos) end - end + end | POG (a) => let val _ = trace wgen ("Testing a proof obligation constraint: \n") val pos = generate_pos model [h] - handle WFCPOG.WFCPOG_WFC_FailedException s => + handle WFCPOG.WFC_FailedMessage s => let val _ = buffer:=((!buffer)^s) in - (h,[(["Exception"],(Variable("x",OclVoid)))]) + [(h,[(["Exception"],(Variable("x",OclVoid)))])] end in case pos of - (h,[(["Exception"],(Variable("x",OclVoid)))]) => + [(h,[(["Exception"],(Variable("x",OclVoid)))])] => let val _ = buffer:=(!buffer)^((name_of h ^ (insert_dots (name_of h)) ^ "[DEPENDING WFC NOT HOLD]\n")) in ([])@(start_tests model wfpos) end - | (wfc,list) => + | wfpo_term_list => let - val _ = buffer:=(!buffer)^((name_of h ^ (insert_dots (name_of h)) ^ "[ " ^ (Int.toString(List.length(list))) ^ " Terms ]\n")) + val ret = List.map (fn (a,b) => + let + val _ = buffer:=((!buffer)^(name_of a)^(insert_dots (name_of a))^"[ "^(Int.toString(List.length(b)))^" Terms ]\n") + in + b + end) wfpo_term_list in - (list)@(start_tests model wfpos) + (ret)@(start_tests model wfpos) end end - + fun test (tc:testcase) wfs pos = let val i_model = ModelImport.import (#uml tc) (#ocl tc) [] @@ -281,7 +286,7 @@ fun runTest_ret_pos name wfs pos = val tc = valOf (List.find (fn a => name = (#name a)) testcases) val _ = trace wgen ("Accessing model ...\n") val s1 = (print_tc tc) - val pos = test tc wfs pos + val pos = List.concat (test tc wfs pos) val _ = buffer:=s1^(!buffer) val _ = if (String.isSubstring "[Error]" (!buffer)) @@ -296,14 +301,14 @@ fun runTests_ret_pos wfs pos = let val _ = trace wgen ("Starts running tests ...\n") val _ = reset_buffer() - val pos = List.concat (List.map (fn a => + val pos = List.concat (List.concat (List.map (fn a => let val s1 = (print_tc a) val _ = buffer:=(!buffer)^s1 val x = (test a wfs pos) in x - end) testcases) + end) testcases)) val _ = if (String.isSubstring "[ERROR]" (!buffer)) then print ((!buffer)^"\n\n !!!!!!!!!! WFCPOG still contains bugs !!!!!!!!!!!!!\n\n\n") diff --git a/su4sml/src/wfcpog/visibility_consistency.sml b/su4sml/src/wfcpog/visibility_consistency.sml index c7fc18a..0d361f8 100644 --- a/su4sml/src/wfcpog/visibility_consistency.sml +++ b/su4sml/src/wfcpog/visibility_consistency.sml @@ -200,7 +200,7 @@ fun check_entity_classifier class model = SOME(aend) => ("Visibility of operation " ^ (name_of_aend aend) ^ " : " ^ (visibility2string a)) | _ => "" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4^s5^s6) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4^s5^s6) end ) ((vis_ops)@(vis_atts)) in @@ -232,7 +232,7 @@ fun check_inheritance_classifier class model = val s3 = "Visibility of the overriden operation : " ^ (visibility2string (#visibility this_op)) ^ ".\n" val s4 = "Visibility of the original operation (located in " ^ (string_of_path (name_of super)) ^ " ) : " ^ (visibility2string (#visibility sop)) ^ ".\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2^s3^s4) + raise WFCPOG.WFC_FailedMessage (s1^s2^s3^s4) end ) mod_ops_super_this val _ = trace function_ends ("WFCPOG_Visibility_Consistency.check_inheritance_visibility_consistency\n") @@ -277,7 +277,7 @@ fun check_runtime_classifier class model = val s1 = "SYNTAX ERROR: Visibility runtime consistency\n\n" val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in operation " ^ a ^ " in the precondition " ^ (opt2string b) ^ " inconsistent modificators.\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end) ops_pre_vis val check_post = @@ -289,7 +289,7 @@ fun check_runtime_classifier class model = val s1 = "SYNTAX ERROR: Visibility runtime consistency\n\n" val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in operation " ^ a ^ " in the postcondition " ^ (opt2string b) ^ " inconsistent modificators.\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end) ops_post_vis val check_inv = List.map (fn (a,b) => @@ -300,7 +300,7 @@ fun check_runtime_classifier class model = val s1 = "SYNTAX ERROR: Visibility runtime consistency\n\n" val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the invariant " ^ (opt2string(a)) ^ "inconsistent modificators.\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end) invs_vis in List.all (fn a => a = true) (check_pre@check_post@check_inv) @@ -327,7 +327,7 @@ fun check_design_classifier class model = val s1 = "SYNTAX ERROR: Visibility design by contract consistency\n\n" val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in operation " ^ a ^ " in the precondition " ^ (opt2string b) ^ " inconsistent modificators.\n" in - raise WFCPOG.WFCPOG_WFC_FailedException (s1^s2) + raise WFCPOG.WFC_FailedMessage (s1^s2) end) ops_pre_vis in List.all (fn a => a = true) check_pre @@ -344,6 +344,7 @@ fun model_entity_consistency wfc_sel (model as (clist,alist)) = val _ = trace function_ends ("WFCPOG_Visibility_Constraint.model_entity_consistency\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s) end fun model_inheritance_consistency wfc_sel (model as (clist,alist)) = @@ -355,6 +356,7 @@ fun model_inheritance_consistency wfc_sel (model as (clist,alist)) = val _ = trace function_ends ("WFCPOG_Visibility_Constraint.model_inheritance_consistency\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s) end fun constraint_check_by_runtime_consistency wfc_sel (model as (clist,alist)) = @@ -366,6 +368,7 @@ fun constraint_check_by_runtime_consistency wfc_sel (model as (clist,alist)) = val _ = trace function_ends ("WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s) end fun constraint_design_by_contract_consistency wfc_sel (model as (clist,alist)) = @@ -377,5 +380,6 @@ fun constraint_design_by_contract_consistency wfc_sel (model as (clist,alist)) = val _ = trace function_calls ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") in res + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException (wfc_sel,s) end end; diff --git a/su4sml/src/wfcpog/wfcpog.sml b/su4sml/src/wfcpog/wfcpog.sml index ac2e3f8..b3b8058 100644 --- a/su4sml/src/wfcpog/wfcpog.sml +++ b/su4sml/src/wfcpog/wfcpog.sml @@ -69,7 +69,9 @@ sig val id_of : wfpo -> wfpo_id val name_of : wfpo -> string - exception WFCPOG_WFC_FailedException of (wfpo * string) + exception WFC_FailedMessage of string + exception WFC_FailedException of (wfpo * string) + end @@ -92,7 +94,8 @@ and wfpo = WFPO of { data : Object.T Datatab.table } -exception WFCPOG_WFC_FailedException of (wfpo * string) +exception WFC_FailedMessage of string +exception WFC_FailedException of (wfpo * string) fun get_data (WFPO w) = #data w fun up_data data' (WFPO{identifier=identifier,name=name,description=description,