From 477adca8d823b084b6345d4d6f2ff2c688e281d0 Mon Sep 17 00:00:00 2001 From: Manuel Krucker Date: Wed, 7 May 2008 10:30:02 +0000 Subject: [PATCH] subconstraint added constructor consistency git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7898 3260e6d1-4efc-4170-b0a7-36055960796d --- su4sml/src/wfcpog/constructor_consistency.sml | 148 +++++++++++------- su4sml/src/wfcpog/test-data.sml | 5 + su4sml/src/wfcpog/wfcpog_registry.sml | 7 +- 3 files changed, 103 insertions(+), 57 deletions(-) diff --git a/su4sml/src/wfcpog/constructor_consistency.sml b/su4sml/src/wfcpog/constructor_consistency.sml index b68e351..30d7046 100644 --- a/su4sml/src/wfcpog/constructor_consistency.sml +++ b/su4sml/src/wfcpog/constructor_consistency.sml @@ -45,9 +45,9 @@ sig (** sub constraint, included in constructor consistency.*) val post_implies_invariant : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list (** sub constraint, included in constructor consistency.*) - val overwrites_old_creators : WFCPOG.wfpo -> Rep.Model -> bool + val override_old_creators : WFCPOG.wfpo -> Rep.Model -> bool (** sub constraint, included in constructor consistency.*) - val attributes_are_inited : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list + val force_initialize_attributes : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list (** Any kind of Exception *) exception WFCPO_ConstructorError of string end @@ -60,7 +60,7 @@ open Rep_Core open Rep open Rep_OclTerm open Rep_OclType - +open Rep_HolOcl_Namespace (* OclParser *) open ModelImport @@ -69,73 +69,113 @@ open WFCPOG_Library exception WFCPO_ConstructorError of string -(* Make a string case insensitive *) - -fun generate_return_value crea_op classifier model = +fun term_post_implies_inv class oper model = let - val invs1 = all_invariants_of classifier model - val invs2 = List.map (fn (a,b) => b) invs1 - val invs = conjugate_terms invs2 - val posts1 = postcondition_of_op crea_op - val posts2 = List.map (fn (a,b) => b) posts1 - val posts = conjugate_terms posts2 + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") + val inv = Predicate (Variable("self",type_of class),type_of class,name_of_inv class,[]) + val post = Predicate (Variable ("self",type_of class),type_of class,name_of_post class oper,args2varargs ((arguments_of_op oper)@[("result",(#result oper))])) + val implies = OperationCall (post,Boolean,["holOclLib","Boolean","implies"],[(inv,Boolean)],Boolean) + val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.term_post_implies_inv\n") in - (["po_cstr"]@["_"]@["post_implies_inv"]@["_"]@(name_of classifier),OperationCall(posts,Boolean,["Boolean","implies"],[(invs,type_of_term invs)],Boolean)) + implies end -fun post_implies_invariant_help [] model = [] - | post_implies_invariant_help (h::class) (model as (clist,alist)) = +fun term_init_attributes class oper model = let - val creas = creation_operations_of h model - val pos = List.map (fn a => generate_return_value a h model) creas - in - pos@(post_implies_invariant_help (class) model) - end - - -fun post_implies_invariant wfpo (model as (clist, alist)) = - let - val _ = trace function_calls ("WP_constructor_CS.post_implies_invariant\n") - val class = removeOclLibrary clist - val res = post_implies_invariant_help class model - val _ = trace function_ends ("WP_constructor_CS.post_implies_invariant\n") + (* + *) in + Variable ("no",OclVoid) + end + +fun check_override_classifier class (model as (clist,alist)) = + let + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") + val creas = creation_operations_of class model + val over_ops = modified_operations_of class model + val check = + List.map (fn a => + if (List.exists (fn b => a = b) over_ops) + then true + else + let + 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) + end) creas + val res = List.all (fn a => a = true) check + val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") + in res end -fun overwrites_old_creators_help [] model = [true] - | overwrites_old_creators_help (h::classes) (model as (clist,alist)) = +fun generate_post_classifier class model = let - val creas = creation_operations_of h model - val over_ops = modified_operations_of h model + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.check_post_classifier\n") + val pos = + List.map (fn a => + let + val term = term_post_implies_inv class a model + val path = ["po_cstr_","post_",(string_of_path (name_of class)),(name_of_op a)] + in + (path,term) + end) (creation_operations_of class model) + val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.check_override_classifier\n") in - (List.all (fn a => List.exists (fn b => b = a) (over_ops)) creas)::(overwrites_old_creators_help classes model) - end - -fun overwrites_old_creators wfpo (model as (clist, alist)) = - let - val class = removeOclLibrary clist - in - List.all (fn a => a) (overwrites_old_creators_help class model) - end - -fun attributes_are_inited_help [] model = [] - | attributes_are_inited_help (h::classes) (model as (clist,alist)) = - let - val _ = trace function_calls ("WP_constructor_CS.attributes_are_inited_help\n") - val creas = creation_operations_of h model - (* TODO: express term *) - val _ = trace function_ends ("WP_constructor_CS.attributes_are_inited_help\n") - in - []:(Path * OclTerm) list + pos end -fun attributes_are_inited wfpo (model as (clist,alist)) = +fun generate_attribute_classifier class model = let - val classes = removeOclLibrary clist + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") + val pos = + List.map (fn a => + let + val term = term_init_attributes class a model + val path = ["po_cstr_","attribute_",(string_of_path (name_of class)),(name_of_op a)] + in + (path,term) + end) (creation_operations_of class model) + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.generate_attribute_classifier\n") in - (attributes_are_inited_help classes model) + pos + end + + +fun override_old_creators wfpo (model as (clist, alist)) = + let + val _ = trace function_calls ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl + val res = List.all (fn a => a = true) (List.map (fn a => check_override_classifier a model) classes) + val _ = trace function_calls ("WFCPOG_Constructor_Consistency.overrides_old_creators\n") + in + res + end + +fun post_implies_invariant wfpo (model as (clist, alist)) = + let + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl + val list = List.concat (List.map (fn a => generate_post_classifier a model) classes) + val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.post_implies_invariant\n") + in + list + end + + +fun force_initialize_attributes wfpo (model as (clist,alist)) = + let + val _ = trace function_calls ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") + val cl = removeOclLibrary clist + val classes = List.filter (fn a => (is_Class a) orelse (is_AssoClass a)) cl + val list = List.concat (List.map (fn a => generate_attribute_classifier a model) classes) + val _ = trace function_ends ("WFCPOG_Constructor_Consistency_Constraint.force_initialize_attributes\n") + in + list end end; diff --git a/su4sml/src/wfcpog/test-data.sml b/su4sml/src/wfcpog/test-data.sml index 3402eb1..582407e 100644 --- a/su4sml/src/wfcpog/test-data.sml +++ b/su4sml/src/wfcpog/test-data.sml @@ -50,6 +50,9 @@ val _ = trace high ("............. refine wfc constraint loaded ...\n") (** ################# **) (** LISKOV CONSTRAINT **) +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 _ = trace high ("............. liskov constraint loaded ...\n") @@ -63,6 +66,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 = get_wfpo supported_pos "po_cstr" val _ = trace high ("............. constructor constraints loaded ...\n") diff --git a/su4sml/src/wfcpog/wfcpog_registry.sml b/su4sml/src/wfcpog/wfcpog_registry.sml index d1537f7..e7452d0 100644 --- a/su4sml/src/wfcpog/wfcpog_registry.sml +++ b/su4sml/src/wfcpog/wfcpog_registry.sml @@ -114,6 +114,7 @@ struct exception WFCPOG_RegistryError of string exception WFCPOG_MethodologyError of string + open Rep_Logger open WFCPOG open Datatab @@ -386,13 +387,13 @@ val supported_pos = [ data = Datatab.empty }, WFCPOG.WFPO{ - identifier = "po_cstr_attr", + identifier = "po_cstr_attribute", name = "WFC Constructor Consistency attributes are inited(subconstraint)", description = "Checks if after the execution of any constructor operation all the attributes are initialized.\n", recommended = false, depends = [], recommends = [], - apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.attributes_are_inited), + apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.force_initialize_attributes), data = Datatab.empty }, WFCPOG.WFPO{ @@ -402,7 +403,7 @@ val supported_pos = [ recommended = false, depends = ["po_cstr_post"], recommends = [], - apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.attributes_are_inited), + apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.force_initialize_attributes), data = Datatab.empty } ,