git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7751 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Manuel Krucker
parent
1de3c190ac
commit
38c9493c48
|
|
@ -48,10 +48,6 @@ sig
|
|||
val overwrites_old_creators : WFCPOG.wfpo -> Rep.Model -> bool
|
||||
(** sub constraint, included in constructor consistency.*)
|
||||
val attributes_are_inited : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
|
||||
(** all wfs of package constructor *)
|
||||
val generate_wfs : WFCPOG.wfpo -> Rep.Model -> bool
|
||||
(** all pos of package constructor *)
|
||||
val generate_pos : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
|
||||
(** Any kind of Exception *)
|
||||
exception WFCPO_ConstructorError of string
|
||||
end
|
||||
|
|
@ -142,23 +138,4 @@ fun attributes_are_inited wfpo (model as (clist,alist)) =
|
|||
in
|
||||
(attributes_are_inited_help classes model)
|
||||
end
|
||||
|
||||
fun generate_wfs wfpo (model:Rep.Model as (clist,alist)) =
|
||||
let
|
||||
val _ = trace function_calls ("WP_constructor_CS.generate_wfs\n")
|
||||
val res = overwrites_old_creators wfpo model
|
||||
val _ = trace function_ends ("WP_constructor_CS.generate_wfs\n")
|
||||
in
|
||||
res
|
||||
end
|
||||
|
||||
fun generate_pos wfpo (model:Rep.Model as (clist,alist)) =
|
||||
let
|
||||
val _ = trace function_calls ("WP_constructor_CS.generate_pos\n")
|
||||
val res1 = post_implies_invariant wfpo model
|
||||
val res2 = attributes_are_inited wfpo model
|
||||
val _ = trace function_ends ("WP_constructor_CS.generate_pos\n")
|
||||
in
|
||||
res1@res2
|
||||
end
|
||||
end;
|
||||
|
|
|
|||
|
|
@ -13,16 +13,18 @@ structure TAX_Data = WFCPOG_Taxonomy_Constraint.WFCPOG_TAX_Data
|
|||
|
||||
|
||||
(** LISKOV CONSTRAINT **)
|
||||
val lsk = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "lsk"
|
||||
val lsk = get_wfpo supported_pos "lsk"
|
||||
val _ = trace high ("............. liskov constraint loaded ...\n")
|
||||
|
||||
|
||||
|
||||
(** INTERFACE CONSTRAINT **)
|
||||
val inf = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "inf"
|
||||
val inf = get_wfpo supported_wfs "wfc_inf"
|
||||
val _ = trace high ("............. interface constraint loaded ...\n")
|
||||
|
||||
(** DATA MODEL CONSTRAINT **)
|
||||
val cm = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "class_model"
|
||||
val sm = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "strong_model"
|
||||
val cm = get_wfpo supported_pos "class_model"
|
||||
val sm = get_wfpo supported_pos "strong_model"
|
||||
val _ = trace high ("............. data model constraint loaded ...\n")
|
||||
|
||||
(** OPERATIONAL CONSTRAINT **)
|
||||
|
|
@ -31,36 +33,40 @@ val om = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "oper_model"
|
|||
val _ = trace high ("............. operational constraint loaded ...\n")
|
||||
*)
|
||||
(** COMMAND/QUERY CONSTRAINT **)
|
||||
val cmd = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "cmd"
|
||||
val quy = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "quy"
|
||||
val cmd = get_wfpo supported_pos "cmd"
|
||||
val quy = get_wfpo supported_pos "quy"
|
||||
val _ = trace high ("............. command/query constraints loaded ...\n")
|
||||
|
||||
(** VISIBILITY CONSTRAINT **)
|
||||
val vis = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "vis"
|
||||
val vis = get_wfpo supported_wfs "wfc_vis"
|
||||
val _ = trace high ("............. visibility constraint loaded ...\n")
|
||||
|
||||
(** REFINEMENT CONSTRAINT **)
|
||||
val rfm_wfc = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "rfm_wfc"
|
||||
val rfm_wfc = get_wfpo supported_wfs "wfc_rfm"
|
||||
val _ = trace high ("............. refinement constraints loaded ...\n")
|
||||
val rfm_pog = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "rfm_pog"
|
||||
val rfm_pog = get_wfpo supported_pos "rfm"
|
||||
val _ = trace high ("............. refinement constraints loaded ...\n")
|
||||
|
||||
(* TAXONOMY CONSTRAINT *)
|
||||
val tax = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "tax"
|
||||
val tax = get_wfpo supported_wfs "wfc_tax"
|
||||
val _ = trace high ("............. taxonomy constraint loaded ...\n")
|
||||
|
||||
val rfm_SC_wfc = WFCPOG_Registry.rename_wfpo "rfm_SC_wfc" (RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])]}) rfm_wfc)
|
||||
val rfm_SC_pog = WFCPOG_Registry.rename_wfpo "rfm_SC_pog" (RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])]}) rfm_pog)
|
||||
|
||||
val md0 = WFCPOG_Registry.rename_wfpo "md0" (TAX_Data.put ({key=9,max_depth=0}) tax)
|
||||
val md1 = WFCPOG_Registry.rename_wfpo "md1" (TAX_Data.put ({key=9,max_depth=1}) tax)
|
||||
val md2 = WFCPOG_Registry.rename_wfpo "md2" (TAX_Data.put ({key=9,max_depth=2}) tax)
|
||||
val md3 = WFCPOG_Registry.rename_wfpo "md3" (TAX_Data.put ({key=9,max_depth=3}) tax)
|
||||
val md4 = WFCPOG_Registry.rename_wfpo "md4" (TAX_Data.put ({key=9,max_depth=4}) tax)
|
||||
val md5 = WFCPOG_Registry.rename_wfpo "md5" (TAX_Data.put ({key=9,max_depth=5}) tax)
|
||||
val md6 = WFCPOG_Registry.rename_wfpo "md6" (TAX_Data.put ({key=9,max_depth=6}) tax)
|
||||
val md7 = WFCPOG_Registry.rename_wfpo "md7" (TAX_Data.put ({key=9,max_depth=7}) tax)
|
||||
val md8 = WFCPOG_Registry.rename_wfpo "md8" (TAX_Data.put ({key=9,max_depth=8}) tax)
|
||||
val rfm_SC_wfc = rename_wfpo "rfm_SC_wfc" (RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])]}) rfm_wfc)
|
||||
val _ = trace high ("............. refine wfc constraint loaded ...\n")
|
||||
val rfm_SC_pog = rename_wfpo "rfm_SC_pog" (RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair04"],["ConcreteSimpleChair02"])]}) rfm_pog)
|
||||
val _ = trace high ("............. refine pog constraint loaded ...\n")
|
||||
|
||||
(*
|
||||
val md0 = rename_wfpo "md0" (TAX_Data.put ({key=8,max_depth=10}) tax)
|
||||
val md1 = rename_wfpo "md1" (TAX_Data.put ({key=9,max_depth=1}) tax)
|
||||
val md2 = rename_wfpo "md2" (TAX_Data.put ({key=9,max_depth=2}) tax)
|
||||
val md3 = rename_wfpo "md3" (TAX_Data.put ({key=9,max_depth=3}) tax)
|
||||
val md4 = rename_wfpo "md4" (TAX_Data.put ({key=9,max_depth=4}) tax)
|
||||
(* val md5 = rename_wfpo "md5" (TAX_Data.put ({key=9,max_depth=5}) tax) *)
|
||||
val md6 = rename_wfpo "md6" (TAX_Data.put ({key=9,max_depth=6}) tax)
|
||||
val md7 = rename_wfpo "md7" (TAX_Data.put ({key=9,max_depth=7}) tax)
|
||||
val md8 = rename_wfpo "md8" (TAX_Data.put ({key=9,max_depth=8}) tax)
|
||||
|
||||
(*
|
||||
val wfs = [inf,vis,md0,md1,md2,md3,md4,md5,md6,md7,md8,rfm_SC_wfc]
|
||||
|
|
@ -74,3 +80,5 @@ val pos = [rfm_SC_pog]
|
|||
|
||||
val wfs = []
|
||||
val pos = [cm,sm]
|
||||
|
||||
*)
|
||||
|
|
|
|||
|
|
@ -41,31 +41,51 @@
|
|||
|
||||
signature WFCPOG_REGISTRY =
|
||||
sig
|
||||
val supported_wfs : WFCPOG.wfpo list
|
||||
val supported_pos : WFCPOG.wfpo list
|
||||
(** Customized wfc and po list, at the beginning empty.*)
|
||||
val wfpos : WFCPOG.wfpo list ref
|
||||
(** Add wfpo to customized list.*)
|
||||
val add_wfpo : WFCPOG.wfpo -> unit
|
||||
(** Delete wfpo from customized list.*)
|
||||
val del_wfpo : WFCPOG.wfpo_id -> unit
|
||||
|
||||
|
||||
(** All the supported well-formedness checks. *)
|
||||
val supported_wfs : WFCPOG.wfpo list
|
||||
(** All the supported proof obligations. *)
|
||||
val supported_pos : WFCPOG.wfpo list
|
||||
|
||||
(** Checks if the wfpo is a well-formedness check. *)
|
||||
val is_wfc : WFCPOG.wfpo -> bool
|
||||
(** Checks if the wfpo is a proof obligation.*)
|
||||
val is_pog : WFCPOG.wfpo -> bool
|
||||
|
||||
(** Checks if a given name is a supported wfc.*)
|
||||
val wf_is_supported_id : WFCPOG.wfpo_id -> bool
|
||||
(** Checks if a given name is a supported po.*)
|
||||
val po_is_supported_id : WFCPOG.wfpo_id -> bool
|
||||
|
||||
val rename_wfpo : string -> WFCPOG.wfpo -> WFCPOG.wfpo
|
||||
val get_wfpo : WFCPOG.wfpo list -> WFCPOG.wfpo_id -> WFCPOG.wfpo
|
||||
|
||||
|
||||
(** Execute a wfc.*)
|
||||
val check_wfc : Rep.Model -> WFCPOG.wfpo -> bool
|
||||
(** Execute a list of wfcs.*)
|
||||
val check_wfcs : Rep.Model -> WFCPOG.wfpo list -> bool
|
||||
|
||||
(** Execute all recommended wfcs.*)
|
||||
val check_recommended_wfcs : Rep.Model -> bool
|
||||
|
||||
|
||||
(** Generate pos for a given wfpo.*)
|
||||
val generate_po : Rep.Model -> WFCPOG.wfpo -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list)
|
||||
(** Generate pos for a list of wfpos.*)
|
||||
val generate_pos : Rep.Model -> WFCPOG.wfpo list -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list) list
|
||||
|
||||
(** Generate all recommended pos.*)
|
||||
val generate_recommended_pos : Rep.Model -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list) list
|
||||
|
||||
(** Argument Wrappers *)
|
||||
(** Create wfpo for wfc max_depth.*)
|
||||
val create_wfc_tax : int -> WFCPOG.wfpo
|
||||
exception WFCPOG_RegistryError of string
|
||||
end
|
||||
|
||||
|
|
@ -157,7 +177,7 @@ val tax_workaround =
|
|||
val supported_wfs = [
|
||||
WFCPOG.WFPO{
|
||||
identifier = "wfc_inf_ster",
|
||||
name = "WFC Interface Consistency (subconstraint)",
|
||||
name = "WFC Interface Consistency consistent stereotypes (subconstraint)",
|
||||
description = "Checks if all operations of an interface don't have the stereotypes 'create' or 'destroy'.\n",
|
||||
recommended = false,
|
||||
depends = [],
|
||||
|
|
@ -167,7 +187,7 @@ val supported_wfs = [
|
|||
},
|
||||
WFCPOG.WFPO{
|
||||
identifier = "wfc_inf_name",
|
||||
name = "WFC Interface Consistency (subconstraint)",
|
||||
name = "WFC Interface Consistency no nameclashes (subconstraint)",
|
||||
description = "Checks for classes inheriting from more than one interface that there are no nameclashes.\n",
|
||||
recommended = false,
|
||||
depends = [],
|
||||
|
|
@ -199,7 +219,7 @@ val supported_wfs = [
|
|||
,
|
||||
WFCPOG.WFPO{
|
||||
identifier = "wfc_rfm",
|
||||
name = "WFOO Refinement",
|
||||
name = "WFC OO Refinement",
|
||||
description = "Checks if public classes of aboriginal package are also public in new package\n",
|
||||
recommended = false,
|
||||
depends = [],
|
||||
|
|
@ -209,12 +229,12 @@ val supported_wfs = [
|
|||
},
|
||||
WFCPOG.WFPO{
|
||||
identifier = "wfc_cstr",
|
||||
name = "Constructor Consistency",
|
||||
description = "Check if public classes of aboriginal are also public in new Package",
|
||||
recommended = false,
|
||||
name = "WFC Constructor Consistency",
|
||||
description = "Checks if a given class overwrites all old creators\n.",
|
||||
recommended = true,
|
||||
depends = [],
|
||||
recommends = [],
|
||||
apply = WFCPOG.WFC(WFCPOG_Refine_Constraint.check_syntax),
|
||||
apply = WFCPOG.WFC(WFCPOG_Constructor_Constraint.overwrites_old_creators),
|
||||
data = Datatab.empty
|
||||
}
|
||||
]
|
||||
|
|
@ -309,6 +329,36 @@ val supported_pos = [
|
|||
recommends = [],
|
||||
apply = WFCPOG.POG(WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency),
|
||||
data = Datatab.empty
|
||||
},
|
||||
WFCPOG.WFPO{
|
||||
identifier = "cstr_post",
|
||||
name = "Constructor Consistency post implies invariants(subconstraint)",
|
||||
description = "Checks if the postcondition of any constructor operation imples the class' invariant.\n",
|
||||
recommended = false,
|
||||
depends = [],
|
||||
recommends = [],
|
||||
apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.post_implies_invariant),
|
||||
data = Datatab.empty
|
||||
},
|
||||
WFCPOG.WFPO{
|
||||
identifier = "cstr_attr",
|
||||
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),
|
||||
data = Datatab.empty
|
||||
},
|
||||
WFCPOG.WFPO{
|
||||
identifier = "cstr",
|
||||
name = "WFC Constructor Consistency (complete)",
|
||||
description = "Checks two subconstraints: \n cstr_post : Checks if after the execution of any constructor operation all the attributes are initialized.\n cstr_attr: Checks if after the execution of any constructor operation all the attributes are initialized.\n",
|
||||
recommended = false,
|
||||
depends = ["cstr_post"],
|
||||
recommends = [],
|
||||
apply = WFCPOG.POG(WFCPOG_Constructor_Constraint.attributes_are_inited),
|
||||
data = Datatab.empty
|
||||
}
|
||||
(*,
|
||||
WFCPOG.WFPO{
|
||||
|
|
|
|||
Loading…
Reference in New Issue