subconstraints query added
git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7951 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Manuel Krucker
parent
446d932ffc
commit
9e8c307793
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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 **)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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",
|
||||
|
|
|
|||
Loading…
Reference in New Issue