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

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7770 3260e6d1-4efc-4170-b0a7-36055960796d

This commit is contained in:
Manuel Krucker 2008-04-28 08:17:52 +00:00
parent 509cefb636
commit 53e2526ae4
9 changed files with 46 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -42,9 +42,9 @@
(** Implementation of the Liskov Substitiution Principle. *) (** Implementation of the Liskov Substitiution Principle. *)
signature WFCPOG_COMMAND_QUERY_CONSTRAINT = signature WFCPOG_COMMAND_QUERY_CONSTRAINT =
sig sig
val ops_are_query : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val ops_are_query : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
val ops_are_command : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val ops_are_command : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
end end
structure WFCPOG_Command_Query_Constraint:WFCPOG_COMMAND_QUERY_CONSTRAINT = structure WFCPOG_Command_Query_Constraint:WFCPOG_COMMAND_QUERY_CONSTRAINT =
struct struct
@ -116,7 +116,7 @@ fun ops_are_query_help [] model = []
| ops_are_query_help (h::classes) (model as (clist,alist)) = | ops_are_query_help (h::classes) (model as (clist,alist)) =
let let
val qops = query_operations_of h model val qops = query_operations_of h model
val x = List.map (fn a => (("quy_"^(string_of_path(name_of h))),post_implies_args_and_self_at_pre a h)) qops 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 in
(x)@(ops_are_query_help classes model) (x)@(ops_are_query_help classes model)
end end
@ -125,7 +125,7 @@ fun ops_are_command_help [] model = []
| ops_are_command_help (h::classes) (model as (clist,alist)) = | ops_are_command_help (h::classes) (model as (clist,alist)) =
let let
val cops = command_operations_of h model val cops = command_operations_of h model
val x = List.map (fn a => (("cmd_"^(string_of_path (name_of h))),post_implies_not_args_or_not_self_at_pre a h)) cops 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 in
(x)@(ops_are_command_help classes model) (x)@(ops_are_command_help classes model)
end end

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

@ -43,11 +43,11 @@
signature WFCPOG_CONSTRUCTOR_CONSTRAINT = signature WFCPOG_CONSTRUCTOR_CONSTRAINT =
sig sig
(** sub constraint, included in constructor consistency.*) (** sub constraint, included in constructor consistency.*)
val post_implies_invariant : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val post_implies_invariant : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** sub constraint, included in constructor consistency.*) (** sub constraint, included in constructor consistency.*)
val overwrites_old_creators : WFCPOG.wfpo -> Rep.Model -> bool val overwrites_old_creators : WFCPOG.wfpo -> Rep.Model -> bool
(** sub constraint, included in constructor consistency.*) (** sub constraint, included in constructor consistency.*)
val attributes_are_inited : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val attributes_are_inited : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** Any kind of Exception *) (** Any kind of Exception *)
exception WFCPO_ConstructorError of string exception WFCPO_ConstructorError of string
end end
@ -81,7 +81,7 @@ fun generate_return_value crea_op classifier model =
val posts2 = List.map (fn (a,b) => b) posts1 val posts2 = List.map (fn (a,b) => b) posts1
val posts = conjugate_terms posts2 val posts = conjugate_terms posts2
in in
(("post_implies_inv_"^(string_of_path (name_of classifier))),OperationCall(posts,Boolean,["Boolean","implies"],[(invs,type_of_term invs)],Boolean)) (["po_cstr"]@["_"]@["post_implies_inv"]@["_"]@(name_of classifier),OperationCall(posts,Boolean,["Boolean","implies"],[(invs,type_of_term invs)],Boolean))
end end
fun post_implies_invariant_help [] model = [] fun post_implies_invariant_help [] model = []
@ -128,7 +128,7 @@ fun attributes_are_inited_help [] model = []
(* TODO: express term *) (* TODO: express term *)
val _ = trace function_ends ("WP_constructor_CS.attributes_are_inited_help\n") val _ = trace function_ends ("WP_constructor_CS.attributes_are_inited_help\n")
in in
[]:(string * OclTerm) list []:(Path * OclTerm) list
end end

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

@ -43,9 +43,9 @@
signature WFCPOG_DATA_MODEL_CONSISTENCY_CONSTRAINT = signature WFCPOG_DATA_MODEL_CONSISTENCY_CONSTRAINT =
sig sig
(** sub constraint, included in liskov.*) (** sub constraint, included in liskov.*)
val class_model_consistency : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val class_model_consistency : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** sub constraint, included in liskov.*) (** sub constraint, included in liskov.*)
val strong_model_consistency : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val strong_model_consistency : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
end end
structure WFCPOG_Data_Model_Consistency_Constraint : WFCPOG_DATA_MODEL_CONSISTENCY_CONSTRAINT = structure WFCPOG_Data_Model_Consistency_Constraint : WFCPOG_DATA_MODEL_CONSISTENCY_CONSTRAINT =
struct struct
@ -103,7 +103,7 @@ fun single_model_consistency (c:Classifier) (model as (clist,alist)) =
fun class_model_consistency_help [] (model as (clist,alist)) = [] fun class_model_consistency_help [] (model as (clist,alist)) = []
| class_model_consistency_help (h::classes) (model as (clist,alist)) = | class_model_consistency_help (h::classes) (model as (clist,alist)) =
(("class_model_"^(string_of_path (name_of h)),single_model_consistency h model)::(class_model_consistency_help classes model)) (["po_class_model_"]@(name_of h),single_model_consistency h model)::(class_model_consistency_help classes model)
fun class_model_consistency wfpo (model as (clist,alist)) = fun class_model_consistency wfpo (model as (clist,alist)) =
let let
@ -118,7 +118,7 @@ fun strong_model_consistency_help classes model =
val terms = List.map (c_allInstance_term) classes val terms = List.map (c_allInstance_term) classes
val n_term = nest_source terms val n_term = nest_source terms
val dummy_body = Variable("dummy_body",DummyT) val dummy_body = Variable("dummy_body",DummyT)
val res = [("strong_model",Iterator("holOclLib.exists",[("\\<tau>",DummyT)],n_term,Boolean,dummy_body,DummyT,Boolean))] val res = [(["po_strong_model"],Iterator("holOclLib.exists",[("\\<tau>",DummyT)],n_term,Boolean,dummy_body,DummyT,Boolean))]
val _ = trace function_ends("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n") val _ = trace function_ends("WFCPOG_Data_Model_Consistency_Constraint.strong_model_consistency\n")
in in
res res

27
su4sml/src/wfcpog/liskov_constraint.sml
View File

@ -55,16 +55,14 @@ sig
val print_liskov_args : Liskov_args -> unit val print_liskov_args : Liskov_args -> unit
(** sub constraint, included in liskov.*) (** sub constraint, included in liskov.*)
val weaken_precondition : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val weaken_precondition : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** sub constraint, included in liskov.*) (** sub constraint, included in liskov.*)
val strengthen_postcondition : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val strengthen_postcondition : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** sub constraint, included in liskov.*) (** sub constraint, included in liskov.*)
val conjugate_invariants : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val conjugate_invariants : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** all three subconstraints together *)
val generate_po : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
end end
structure WFCPOG_Liskov_Constraint : WFCPOG_LISKOV_CONSTRAINT = structure WFCPOG_Liskov_Constraint : WFCPOG_LISKOV_CONSTRAINT =
struct struct
@ -159,7 +157,7 @@ fun weaken_precondition_help [] model = []
(* (operation of subclass, classifier of super class) *) (* (operation of subclass, classifier of super class) *)
val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo
(* proofs obligation for classifier [(term,constraint info)] *) (* proofs obligation for classifier [(term,constraint info)] *)
val pos = List.map (fn (a,b) => (((path_to_string (name_of class) "_")), val pos = List.map (fn (a,b) => (["po_lsk_pre_"]@(name_of class)@["_"]@[name_of_op a],
generate_return_value weaken_pre a class b model)) raw_po generate_return_value weaken_pre a class b model)) raw_po
in in
pos@(weaken_precondition_help clist model) pos@(weaken_precondition_help clist model)
@ -180,7 +178,7 @@ fun strengthen_postcondition_help [] model = []
(* (operation of subclass, classifier of super class) *) (* (operation of subclass, classifier of super class) *)
val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo
(* proof obligations for classifier [(term,constraint info)] *) (* proof obligations for classifier [(term,constraint info)] *)
val pos = List.map (fn (a,b) => (((path_to_string (name_of class) "_")), val pos = List.map (fn (a,b) => (["po_lsk_post"]@["_"]@(name_of class)@["_"]@[name_of_op a],
generate_return_value strengthen_post a class b model)) raw_po generate_return_value strengthen_post a class b model)) raw_po
in in
pos@(strengthen_postcondition_help clist model) pos@(strengthen_postcondition_help clist model)
@ -203,7 +201,7 @@ fun conjugate_invariants_help [] model = []
in in
if (List.length(invs) = 0) if (List.length(invs) = 0)
then (conjugate_invariants_help clist model) then (conjugate_invariants_help clist model)
else (((path_to_string (name_of class) "_")), else (["po_lsk_inv"]@["_"]@(name_of class)@["_"],
conjugate_terms invs)::(conjugate_invariants_help clist model) conjugate_terms invs)::(conjugate_invariants_help clist model)
end end
@ -216,18 +214,5 @@ fun conjugate_invariants wfpo (model as (clist,alist)) =
conjugate_invariants_help cl model conjugate_invariants_help cl model
end end
fun generate_po wfpo (model as (clist,alist)) =
let
val msg1 = ("\n\ngenerate_po: \n")
val x1 = weaken_precondition wfpo model
val msg2 = ("weaken the precondition: " ^ Int.toString(List.length(x1)) ^ " terms generated.\n")
val x2 = strengthen_postcondition wfpo model
val msg3 = ("strengthen the postcondition: " ^ Int.toString(List.length(x2)) ^ " terms generated.\n")
val x3 = conjugate_invariants wfpo model
val msg4 = ("conjugate the invariants: " ^ Int.toString(List.length(x3)) ^ " terms generated.\n\n")
val _ = trace wgen (msg1^msg2^msg3^msg4)
in
x1@x2@x3
end
end end

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

@ -53,7 +53,7 @@ sig
val check_syntax : WFCPOG.wfpo -> Rep.Model -> bool val check_syntax : WFCPOG.wfpo -> Rep.Model -> bool
val generate_pos : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list val generate_pos : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
exception WFCPOG_RefineError of string exception WFCPOG_RefineError of string
exception ClassGroupError of Rep_Core.Classifier list * string exception ClassGroupError of Rep_Core.Classifier list * string
@ -340,7 +340,7 @@ fun refine_operation abs_oper conc_oper abs_class conc_class model =
val refine = OperationCall(S,DummyT,["holOclLib","methodology","refinement","OclForwardRefinement"],[(T,DummyT),(R,DummyT)],Boolean) val refine = OperationCall(S,DummyT,["holOclLib","methodology","refinement","OclForwardRefinement"],[(T,DummyT),(R,DummyT)],Boolean)
val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_classifier\n") val _ = trace function_ends ("WFCPOG_Refine_Constraint.refine_classifier\n")
in in
(("refine_"^(string_of_path (package_of abs_class))^"_"^(string_of_path (package_of conc_class))^"_"^(name_of_op abs_oper)),refine) (["po_refine_"]@(package_of abs_class)@["__"]@(package_of conc_class)@["_"]@[name_of_op abs_oper],refine)
end end
fun refine_classifier abs_class conc_class model = fun refine_classifier abs_class conc_class model =

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

@ -13,7 +13,7 @@ structure TAX_Data = WFCPOG_Taxonomy_Constraint.WFCPOG_TAX_Data
(** LISKOV CONSTRAINT **) (** LISKOV CONSTRAINT **)
val lsk = get_wfpo supported_pos "lsk" val lsk = get_wfpo supported_pos "po_lsk"
val _ = trace high ("............. liskov constraint loaded ...\n") val _ = trace high ("............. liskov constraint loaded ...\n")
@ -23,8 +23,8 @@ val inf = get_wfpo supported_wfs "wfc_inf"
val _ = trace high ("............. interface constraint loaded ...\n") val _ = trace high ("............. interface constraint loaded ...\n")
(** DATA MODEL CONSTRAINT **) (** DATA MODEL CONSTRAINT **)
val cm = get_wfpo supported_pos "class_model" val cm = get_wfpo supported_pos "po_class_model"
val sm = get_wfpo supported_pos "strong_model" val sm = get_wfpo supported_pos "po_strong_model"
val _ = trace high ("............. data model constraint loaded ...\n") val _ = trace high ("............. data model constraint loaded ...\n")
(** OPERATIONAL CONSTRAINT **) (** OPERATIONAL CONSTRAINT **)
@ -33,8 +33,8 @@ val om = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "oper_model"
val _ = trace high ("............. operational constraint loaded ...\n") val _ = trace high ("............. operational constraint loaded ...\n")
*) *)
(** COMMAND/QUERY CONSTRAINT **) (** COMMAND/QUERY CONSTRAINT **)
val cmd = get_wfpo supported_pos "cmd" val cmd = get_wfpo supported_pos "po_cmd"
val quy = get_wfpo supported_pos "quy" val quy = get_wfpo supported_pos "po_quy"
val _ = trace high ("............. command/query constraints loaded ...\n") val _ = trace high ("............. command/query constraints loaded ...\n")
(** VISIBILITY CONSTRAINT **) (** VISIBILITY CONSTRAINT **)
@ -44,7 +44,7 @@ val _ = trace high ("............. visibility constraint loaded ...\n")
(** REFINEMENT CONSTRAINT **) (** REFINEMENT CONSTRAINT **)
val rfm_wfc = get_wfpo supported_wfs "wfc_rfm" val rfm_wfc = get_wfpo supported_wfs "wfc_rfm"
val _ = trace high ("............. refinement constraints loaded ...\n") val _ = trace high ("............. refinement constraints loaded ...\n")
val rfm_pog = get_wfpo supported_pos "rfm" val rfm_pog = get_wfpo supported_pos "po_rfm"
val _ = trace high ("............. refinement constraints loaded ...\n") val _ = trace high ("............. refinement constraints loaded ...\n")
(* TAXONOMY CONSTRAINT *) (* TAXONOMY CONSTRAINT *)

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

@ -5,9 +5,9 @@ sig
(** Executes a specified (string fst arg) test and returns a text output.*) (** Executes a specified (string fst arg) test and returns a text output.*)
val runTest : string -> WFCPOG.wfpo list -> WFCPOG.wfpo list -> unit val runTest : string -> WFCPOG.wfpo list -> WFCPOG.wfpo list -> unit
(** Executes a test on all (default) models and returns the proof obligations.*) (** Executes a test on all (default) models and returns the proof obligations.*)
val execTests : WFCPOG.wfpo list -> WFCPOG.wfpo list -> (string * Rep_OclTerm.OclTerm) list val execTests : WFCPOG.wfpo list -> WFCPOG.wfpo list -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** Executes a specified (string fst arg) test and returns the proof obligations.*) (** Executes a specified (string fst arg) test and returns the proof obligations.*)
val execTest : string -> WFCPOG.wfpo list -> WFCPOG.wfpo list -> (string * Rep_OclTerm.OclTerm) list val execTest : string -> WFCPOG.wfpo list -> WFCPOG.wfpo list -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
(** Set Control.Print.printDepth. *) (** Set Control.Print.printDepth. *)
val set_printDepth : int -> unit val set_printDepth : int -> unit
(** Set Control.Print.printLength. *) (** Set Control.Print.printLength. *)

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

@ -45,7 +45,7 @@ sig
type wfpo_id = string type wfpo_id = string
datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool
| POG of wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list | POG of wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
and and
wfpo = WFPO of { wfpo = WFPO of {
identifier : wfpo_id, (* identifier *) identifier : wfpo_id, (* identifier *)
@ -79,7 +79,7 @@ struct
type wfpo_id = string type wfpo_id = string
datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool
| POG of wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list | POG of wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
and wfpo = WFPO of { and wfpo = WFPO of {
identifier : wfpo_id, (* identifier *) identifier : wfpo_id, (* identifier *)
name : string, (* short description (for output) *) name : string, (* short description (for output) *)

32
su4sml/src/wfcpog/wfcpog_registry.sml
View File

@ -90,12 +90,12 @@ sig
val check_recommended_wfcs : Rep.Model -> bool val check_recommended_wfcs : Rep.Model -> bool
(** Generate pos for a given wfpo.*) (** Generate pos for a given wfpo.*)
val generate_po : Rep.Model -> WFCPOG.wfpo -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list) val generate_po : Rep.Model -> WFCPOG.wfpo -> (WFCPOG.wfpo * (Rep_OclType.Path * Rep_OclTerm.OclTerm) list)
(** Generate pos for a list of wfpos.*) (** Generate pos for a list of wfpos.*)
val generate_pos : Rep.Model -> WFCPOG.wfpo list -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list) list val generate_pos : Rep.Model -> WFCPOG.wfpo list -> (WFCPOG.wfpo * (Rep_OclType.Path * Rep_OclTerm.OclTerm) list) list
(** Generate all recommended pos.*) (** Generate all recommended pos.*)
val generate_recommended_pos : Rep.Model -> (WFCPOG.wfpo * (string * Rep_OclTerm.OclTerm) list) list val generate_recommended_pos : Rep.Model -> (WFCPOG.wfpo * (Rep_OclType.Path * Rep_OclTerm.OclTerm) list) list
(** Argument Wrappers *) (** Argument Wrappers *)
(** Create wfpo for wfc max_depth.*) (** Create wfpo for wfc max_depth.*)
@ -255,7 +255,7 @@ val supported_wfs = [
val supported_pos = [ val supported_pos = [
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "lsk_pre", identifier = "po_lsk_pre",
name = "Liskov weaken_precondition", name = "Liskov weaken_precondition",
description = "Generate Proof Obligations for weaking precondition", description = "Generate Proof Obligations for weaking precondition",
recommended = false, recommended = false,
@ -265,7 +265,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "lsk_post", identifier = "po_lsk_post",
name = "Liskov strengthen_postcondition", (* short description (for output) *) name = "Liskov strengthen_postcondition", (* short description (for output) *)
description = "Generate Proof Obligations following from strengthen_postcondition", description = "Generate Proof Obligations following from strengthen_postcondition",
recommended = false, recommended = false,
@ -275,7 +275,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "lsk_inv", identifier = "po_lsk_inv",
name = "Liskov conjugate_invariants", name = "Liskov conjugate_invariants",
description = "Generate Proof Obligations following from conjugate_invariants", description = "Generate Proof Obligations following from conjugate_invariants",
recommended = false, recommended = false,
@ -285,17 +285,17 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "lsk", identifier = "po_lsk",
name = "Liskov's subtitution principle", name = "Liskov's subtitution principle",
description = "Generate Proof Obligations following the idea from Barbara Liskov", description = "Generate Proof Obligations following the idea from Barbara Liskov",
recommended = true, recommended = true,
depends = ["lsk_pre","lsk_post"], depends = ["po_lsk_pre","po_lsk_post"],
recommends = [], recommends = [],
apply = WFCPOG.POG(WFCPOG_Liskov_Constraint.conjugate_invariants), apply = WFCPOG.POG(WFCPOG_Liskov_Constraint.conjugate_invariants),
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "rfm", identifier = "po_rfm",
name = "OO Refinement", name = "OO Refinement",
description = "Generate Proof Obligations for OO data refinement", description = "Generate Proof Obligations for OO data refinement",
recommended = true, recommended = true,
@ -305,7 +305,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "cmd", (* identifier *) identifier = "po_cmd", (* identifier *)
name = "Query Command Constraint", name = "Query Command Constraint",
description = "Check if operations which are declared as command are really commands", description = "Check if operations which are declared as command are really commands",
recommended = false, recommended = false,
@ -315,7 +315,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "quy", (* identifier *) identifier = "po_quy", (* identifier *)
name = "Query Command Constraint", name = "Query Command Constraint",
description = "Check if operations which are declared as queries are really queries", description = "Check if operations which are declared as queries are really queries",
recommended = false, recommended = false,
@ -325,7 +325,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "class_model", (* identifier *) identifier = "po_class_model", (* identifier *)
name = "Data model consistency: class model", name = "Data model consistency: class model",
description = "Data model consistency: a classes should be able to be instantiated from a state.", description = "Data model consistency: a classes should be able to be instantiated from a state.",
recommended = false, recommended = false,
@ -335,7 +335,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "strong_model", (* identifier *) identifier = "po_strong_model", (* identifier *)
name = "Data model consistency: strong model", name = "Data model consistency: strong model",
description = "Data model consistency; all classes should be able to be instantiated from a state.", description = "Data model consistency; all classes should be able to be instantiated from a state.",
recommended = false, recommended = false,
@ -345,7 +345,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "cstr_post", identifier = "po_cstr_post",
name = "Constructor Consistency post implies invariants(subconstraint)", name = "Constructor Consistency post implies invariants(subconstraint)",
description = "Checks if the postcondition of any constructor operation imples the class' invariant.\n", description = "Checks if the postcondition of any constructor operation imples the class' invariant.\n",
recommended = false, recommended = false,
@ -355,7 +355,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "cstr_attr", identifier = "po_cstr_attr",
name = "WFC Constructor Consistency attributes are inited(subconstraint)", name = "WFC Constructor Consistency attributes are inited(subconstraint)",
description = "Checks if after the execution of any constructor operation all the attributes are initialized.\n", description = "Checks if after the execution of any constructor operation all the attributes are initialized.\n",
recommended = false, recommended = false,
@ -365,7 +365,7 @@ val supported_pos = [
data = Datatab.empty data = Datatab.empty
}, },
WFCPOG.WFPO{ WFCPOG.WFPO{
identifier = "cstr", identifier = "po_cstr",
name = "WFC Constructor Consistency (complete)", 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", 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, recommended = false,