diff --git a/su4sml/src/wfcpog/command_query_consistency.sml b/su4sml/src/wfcpog/command_query_consistency.sml index 1f79ccd..8618d48 100644 --- a/su4sml/src/wfcpog/command_query_consistency.sml +++ b/su4sml/src/wfcpog/command_query_consistency.sml @@ -42,9 +42,19 @@ (** Implementation of the Liskov Substitiution Principle. *) signature WFCPOG_COMMAND_QUERY_CONSTRAINT = sig - val ops_are_query : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list - - val ops_are_command : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list + (** + * All OCL-formulas should only contain operations with are + * side-effect free. *) + val strong_is_query : WFCPOG.wfpo -> Rep.Model -> bool + (** + * All operations declared to be side-effect free should only contain + * OCL-formulas which are side-effect free. + *) + val weak_is_query : WFCPOG.wfpo -> Rep.Model -> bool + (** + * ? + *) +(* val modified_only : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list *) end structure WFCPOG_Command_Query_Constraint:WFCPOG_COMMAND_QUERY_CONSTRAINT = struct @@ -55,7 +65,7 @@ open Rep_Core open Rep_OclTerm open Rep_OclType open Rep2String - +open Ocl2String (* oclparser *) open ModelImport @@ -66,82 +76,111 @@ exception WFCPO_QueryCommandError of string -fun post_implies_args_and_self_at_pre oper class = +fun check_weak_classifier class (model as (clist,alist)) = let - val posts = List.map (fn (a,b) => b) (postcondition_of_op oper) - val fst = conjugate_terms posts - val args = arguments_of_op oper - val args2term = List.map (fn (a,b) => Variable(a,b)) args - val arg_terms = List.map (fn a => - let - val ta = type_of_term a - val x = OperationCall (a,ta,["oclLib","OclAny","atPre"],[],ta) - in - OperationCall (a,ta,["oclLib","Boolean","="],[(x,type_of_term x)],Boolean) - end - ) args2term - val selft = type_of class - val self = Variable("self",selft) - val self_term_help = OperationCall (self,selft,["oclLib","OclAny","atPre"],[],selft) - val self_term = OperationCall (self,selft,["oclLib","OclAny","="],[(self_term_help,type_of_term self_term_help)],Boolean) - val snd = conjugate_terms (self_term::arg_terms) + val ops = query_operations_of class model + val op_posts = List.map (fn a => (a,postcondition_of_op a)) ops + val op_pres = List.map (fn a => (a,precondition_of_op a)) ops + val check_pres = List.map (fn (oper,pres) => + (List.all (fn (a,b) => + if (side_effect_free b model) + then true + else + let + val s1 = "WFC ERROR: Command/Query constraint\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the operatin "^(name_of_op oper)^" the precondition " ^ (opt2string a) ^ " with the term "^(ocl2string false b)^" a call to an operation which is not isQuery.\n" + in + raise WFCPOG.WFC_FailedMessage (s1^s2) + end + ) pres) + ) op_pres + val check_posts = List.map (fn (oper,posts) => + (List.all (fn (a,b) => + if (side_effect_free b model) + then true + else + let + val s1 = "WFC ERROR: Command/Query constraint\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the operation "^(name_of_op oper)^" postcondition " ^ (opt2string a) ^ " with the term "^(ocl2string false b)^" a call to an operation which is not isQuery.\n" + in + raise WFCPOG.WFC_FailedMessage (s1^s2) + end + ) posts) + ) op_posts in - OperationCall(fst,Boolean,["oclLib","Boolean","implies"],[(snd,Boolean)],Boolean) + List.all (fn a => a = true) (check_pres@check_posts) + end + + +fun check_strong_classifier class (model as (clist,alist)) = + let + val ops = local_operations_of class + val invs = local_invariants_of class + val op_posts = List.map (fn a => (a,postcondition_of_op a)) ops + val op_pres = List.map (fn a => (a,precondition_of_op a)) ops + val check_pres = List.map (fn (oper,pres) => + (List.all (fn (a,b) => + if (side_effect_free b model) + then true + else + let + val s1 = "WFC ERROR: Command/Query constraint\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the operation "^(name_of_op oper)^" precondition " ^ (opt2string a) ^ " with the term "^(ocl2string false b)^" a call to an operation which is not isQuery.\n" + in + raise WFCPOG.WFC_FailedMessage (s1^s2) + end + ) pres) + ) op_pres + val check_posts = List.map (fn (oper,posts) => + (List.all (fn (a,b) => + if (side_effect_free b model) + then true + else + let + val s1 = "WFC ERROR: Command/Query constraint\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the operation "^(name_of_op oper)^" postcondition " ^ (opt2string a) ^ " with the term "^(ocl2string false b)^" a call to an operation which is not isQuery.\n" + in + raise WFCPOG.WFC_FailedMessage (s1^s2) + end + ) posts) + ) op_posts + val check_invs = List.all (fn (a,b) => + if (side_effect_free b model) + then true + else + let + val s1 = "WFC ERROR: Command/Query constraint\n\n" + val s2 = "Classifier " ^ (string_of_path (name_of class)) ^ " has in the invariant " ^ (opt2string a) ^ " with the term "^(ocl2string false b)^" a call to an operation which is not isQuery.\n" + in + raise WFCPOG.WFC_FailedMessage (s1^s2) + end + ) invs + in + List.all (fn a => a = true) (check_pres@check_posts@[check_invs]) end -fun post_implies_not_args_or_not_self_at_pre oper class = +fun weak_is_query po (model as (clist,alist)) = let - val posts = List.map (fn (a,b) => b) (postcondition_of_op oper) - val fst = conjugate_terms posts - val args = arguments_of_op oper - val args2term = List.map (fn (a,b) => Variable(a,b)) args - val arg_terms = List.map (fn a => - let - val ta = type_of_term a - val x = OperationCall (a,ta,["oclLib","OclAny","atPre"],[],ta) - in - OperationCall (a,ta,["oclLib","OclAny","<>"],[(x,type_of_term x)],Boolean) - end - ) args2term - val selft = type_of class - val self = Variable("self",selft) - val self_term_help = OperationCall (self,selft,["oclLib","OclAny","atPre"],[],selft) - val self_term = OperationCall (self,selft,["oclLib","OclAny","<>"],[(self_term_help,type_of_term self_term_help)],Boolean) - val snd = disjugate_terms (self_term::arg_terms) + val _ = trace function_calls ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val classes = removeOclLibrary clist + val res = List.all (fn a => a = true) (List.map (fn a => check_weak_classifier a model + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException(po,s)) classes) + val _ = trace function_ends ("WFCPOG_Command_Query_Constraint.strong_is_query\n") in - OperationCall(fst,Boolean,["oclLib","Boolean","implies"],[(snd,Boolean)],Boolean) + res end -fun ops_are_query_help [] model = [] - | ops_are_query_help (h::classes) (model as (clist,alist)) = - let - val qops = query_operations_of h model - val x = List.map (fn a => (["po_quy_"]@(name_of h)@[name_of_op a],post_implies_args_and_self_at_pre a h)) qops - in - (x)@(ops_are_query_help classes model) - end -fun ops_are_command_help [] model = [] - | ops_are_command_help (h::classes) (model as (clist,alist)) = - let - val cops = command_operations_of h model - val x = List.map (fn a => (["po_cmd_"]@(name_of h)@[name_of_op a],post_implies_not_args_or_not_self_at_pre a h)) cops - in - (x)@(ops_are_command_help classes model) - end -fun ops_are_query wfpo (model:Rep.Model as (clist,alist)) = +fun strong_is_query po (model as (clist,alist)) = let - val class = removeOclLibrary clist + val _ = trace function_calls ("WFCPOG_Command_Query_Constraint.strong_is_query\n") + val classes = removeOclLibrary clist + val res = List.all (fn a => a = true) (List.map (fn a => check_strong_classifier a model + handle WFCPOG.WFC_FailedMessage s => raise WFCPOG.WFC_FailedException(po,s)) classes) + val _ = trace function_ends ("WFCPOG_Command_Query_Constraint.strong_is_query\n") in - ops_are_query_help class model - end - -fun ops_are_command wfpo (model:Rep.Model as (clist,alist)) = - let - val class = removeOclLibrary clist - in - - ops_are_command_help class model + res end end; + diff --git a/su4sml/src/wfcpog/test-data.sml b/su4sml/src/wfcpog/test-data.sml index 1e905ae..53f1cf7 100644 --- a/su4sml/src/wfcpog/test-data.sml +++ b/su4sml/src/wfcpog/test-data.sml @@ -28,15 +28,13 @@ val wfc_vis_class = get_wfpo supported_wfs "wfc_vis_class" val wfc_vis_inheritance = get_wfpo supported_wfs "wfc_vis_inheritance" val wfc_vis_runtime = get_wfpo supported_wfs "wfc_vis_runtime" val wfc_vis_design_by_contract = get_wfpo supported_wfs "wfc_vis_design_by_contract" -val wfc_vis = get_wfpo supported_wfs "wfc_vis" +val wfc_vis_all = get_wfpo supported_wfs "wfc_vis_all" val _ = trace high ("............. visibility constraint loaded ...\n") (* TAXONOMY CONSTRAINT *) val wfc_tax = get_wfpo supported_wfs "wfc_tax" -val _ = trace high ("............. taxonomy constraint loaded ...\n") - val wfc_tax_5 = rename_wfpo "wfc_tax_5" (TAX_Data.put ({key=2,max_depth=5}) wfc_tax) - +val _ = trace high ("............. taxonomy constraint loaded ...\n") (** REFINEMENT CONSTRAINT **) val wfc_rfm = get_wfpo supported_wfs "wfc_rfm" @@ -45,6 +43,9 @@ val wfc_rfm_SC = rename_wfpo "wfc_rfm_SC" (RFM_Data.put ({key=10,rfm_tuple=(["Ab val wfc_rfm_SR= rename_wfpo "wfc_rfm_SR" (RFM_Data.put ({key=10,rfm_tuple=(["AbstractOverriding"],["ConcreteOverriding"])}) wfc_rfm) val _ = trace high ("............. refine wfc constraint loaded ...\n") +(** QUERY CONSISTENCY **) +val wfc_quy_strong = get_wfpo supported_wfs "wfc_quy_strong" +val wfc_quy_weak = get_wfpo supported_wfs "wfc_quy_weak" (** ################# **) @@ -55,7 +56,7 @@ val _ = trace high ("............. refine wfc constraint loaded ...\n") val po_lsk_pre = get_wfpo supported_pos "po_lsk_pre" val po_lsk_post = get_wfpo supported_pos "po_lsk_post" val po_lsk_inv = get_wfpo supported_pos "po_lsk_inv" -val po_lsk = get_wfpo supported_pos "po_lsk" +val po_lsk_all = get_wfpo supported_pos "po_lsk_all" val _ = trace high ("............. liskov constraint loaded ...\n") (** DATA MODEL CONSTRAINT **) @@ -70,12 +71,14 @@ val _ = trace high ("............. operational constraint loaded ...\n") (** CONSTRUCTOR CONSTRAINT **) 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 po_cstr_all = get_wfpo supported_pos "po_cstr_all" val _ = trace high ("............. constructor constraints loaded ...\n") (** COMMAND/QUERY CONSTRAINT **) -val po_cmd = get_wfpo supported_pos "po_cmd" +(* +val po_cmd = get_wfpo supported_pos "po_" val po_quy = get_wfpo supported_pos "po_quy" +*) val _ = trace high ("............. command/query constraints loaded ...\n") (** REFINEMENT CONSTRAINT **) diff --git a/su4sml/src/wfcpog/visibility_consistency.sml b/su4sml/src/wfcpog/visibility_consistency.sml index cf92e01..36dfc6e 100644 --- a/su4sml/src/wfcpog/visibility_consistency.sml +++ b/su4sml/src/wfcpog/visibility_consistency.sml @@ -372,7 +372,7 @@ fun constraint_check_by_runtime_consistency wfc_sel (model as (clist,alist)) = res end -fun constraint_design_by_contract_consistency wfc_sel (model as (clist,alist)) = +fun constraint_design_by_contract_consistency wfc_sel (model as (clist,alist)) = let val _ = trace function_calls ("WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency\n") val cl = removeOclLibrary clist diff --git a/su4sml/src/wfcpog/wfcpog_registry.sml b/su4sml/src/wfcpog/wfcpog_registry.sml index 8b42963..445c4c3 100644 --- a/su4sml/src/wfcpog/wfcpog_registry.sml +++ b/su4sml/src/wfcpog/wfcpog_registry.sml @@ -284,6 +284,26 @@ val supported_wfs = [ recommends = [], apply = WFCPOG.WFC(WFCPOG_Constructor_Constraint.override_old_creators), data = Datatab.empty + }, + WFCPOG.WFPO{ + identifier = "wfc_quy_strong", + name = "WFC Command Query Constraint", + description = "Checks if all ocl formualas just contains operationcalls which are isQuery.\n", + recommended = false, + depends = [], + recommends = [], + apply = WFCPOG.WFC(WFCPOG_Command_Query_Constraint.strong_is_query), + data = Datatab.empty + }, + WFCPOG.WFPO{ + identifier = "wfc_quy_weak", + name = "WFC Command Query Constraint", + description = "Checks if operations declared to be isQuery just contains ocl formulas which contain just operationcalls which are isQuery.\n", + recommended = false, + depends = [], + recommends = [], + apply = WFCPOG.WFC(WFCPOG_Command_Query_Constraint.weak_is_query), + data = Datatab.empty } ] @@ -337,27 +357,17 @@ val supported_pos = [ recommends = [], apply = WFCPOG.POG(WFCPOG_Refine_Constraint.generate_pos), data = Datatab.empty - }, + },(* WFCPOG.WFPO{ - identifier = "po_cmd", (* identifier *) + identifier = "po_cmd", name = "Query Command Constraint", description = "Check if operations which are declared as command are really commands", recommended = false, depends = [], recommends = [], - apply = WFCPOG.POG(WFCPOG_Command_Query_Constraint.ops_are_command), + apply = WFCPOG.POG(WFCPOG_Command_Query_Constraint.semantics), data = Datatab.empty - }, - WFCPOG.WFPO{ - identifier = "po_quy", (* identifier *) - name = "Query Command Constraint", - description = "Check if operations which are declared as queries are really queries", - recommended = false, - depends = [], - recommends = [], - apply = WFCPOG.POG(WFCPOG_Command_Query_Constraint.ops_are_query), - data = Datatab.empty - }, + },*) WFCPOG.WFPO{ identifier = "po_class_model", (* identifier *) name = "Data model consistency: class model",