HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

new exception added 

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7924 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Manuel Krucker 2008-05-09 00:19:36 +00:00
parent 5635051340
commit 7e35a497fc
9 changed files with 62 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
su4sml/src/wfcpog/constructor_consistency.sml
View File

@ -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)) =

12
su4sml/src/wfcpog/interface_consistency.sml
View File

@ -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;

8
su4sml/src/wfcpog/load_model.sml
View File

@ -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()

11
su4sml/src/wfcpog/refine_constraint.sml
View File

@ -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 =

3
su4sml/src/wfcpog/taxonomy_consistency.sml
View File

@ -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;

10
su4sml/src/wfcpog/test-data.sml
View File

@ -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]

31
su4sml/src/wfcpog/test-suite.sml
View File

@ -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")

16
su4sml/src/wfcpog/visibility_consistency.sml
View File

@ -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;

7
su4sml/src/wfcpog/wfcpog.sml
View File

@ -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,