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

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

This commit is contained in:
Manuel Krucker 2008-05-12 15:16:08 +00:00
parent 22ac7ba523
commit 88b844f45a
6 changed files with 37 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -87,7 +87,7 @@ fun check_weak_classifier class (model as (clist,alist)) =
then true
else
let
val s1 = "WFC ERROR: Command/Query constraint\n\n"
val s1 = "WFC ERROR: Weak 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)
@ -100,7 +100,7 @@ fun check_weak_classifier class (model as (clist,alist)) =
then true
else
let
val s1 = "WFC ERROR: Command/Query constraint\n\n"
val s1 = "WFC ERROR: Weak 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)
@ -124,7 +124,7 @@ fun check_strong_classifier class (model as (clist,alist)) =
then true
else
let
val s1 = "WFC ERROR: Command/Query constraint\n\n"
val s1 = "WFC ERROR: Strong 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)
@ -137,7 +137,7 @@ fun check_strong_classifier class (model as (clist,alist)) =
then true
else
let
val s1 = "WFC ERROR: Command/Query constraint\n\n"
val s1 = "WFC ERROR: Strong 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)
@ -149,7 +149,7 @@ fun check_strong_classifier class (model as (clist,alist)) =
then true
else
let
val s1 = "WFC ERROR: Command/Query constraint\n\n"
val s1 = "WFC ERROR: Strong 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)

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

@ -83,7 +83,10 @@ fun term_post_implies_inv class oper model =
fun term_init_attributes class oper model =
let
(*
val atts = all_attributes_of class model
val post = Predicate (Variable ("self",type_of class),type_of class,name_of_post class oper,args2varargs ((arguments_of_op oper)@[("result",(#result oper))]))
(* TODO:
* for all attributes: self.att_name = soll definiert sein
*)
in
Variable ("no",OclVoid)

21
su4sml/src/wfcpog/load_model.sml
View File

@ -21,20 +21,21 @@ val zargo = prefix^"simple_rfm/simple_rfm.zargo"
val ocl = prefix^"simple_rfm/simple_rfm.ocl"
val remP = []
*)
(*
val zargo = "../../../../examples/meeting/Meeting.zargo"
(*
val zargo = prefix^"meeting/Meeting.zargo"
val ocl = ""
val remP = []
*)
(*
val zargo = "../../../hol-ocl/examples/SimpleChair/SimpleChair.zargo"
val ocl = "../../../hol-ocl/examples/SimpleChair/AbstractSimpleChair04.ocl"
val remP = ["AbstractSimpleChair02", "AbstractSimpleChair03","AbstractSimpleChair01","ConcreteSimpleChair01"] ;
*)
(** EBANK **)
(*
val zargo = "../../../examples/ebank/ebank.zargo"
val ocl="../../../examples/ebank/ebank.ocl"
val zargo = prefix^"ebank/ebank.zargo"
val ocl=prefix^"ebank/ebank.ocl"
val remP = []
*)
@ -86,11 +87,11 @@ val zargo = "../../../hol-ocl/examples/overriding/overriding.zargo"
val ocl="../../../hol-ocl/examples/overriding/overriding.ocl"
val remP = []
*)
(*
val zargo = "../../../hol-ocl/examples/stack_manu/stack.zargo"
val ocl="../../../hol-ocl/examples/stack_manu/stack.ocl"
val zargo = prefix^"stack_manu/stack.zargo"
val ocl=prefix^"stack_manu/stack.ocl"
val remP = []
*)
(** import model *)
val XMI = parseUML zargo
val _ = init_offset()

6
su4sml/src/wfcpog/status.txt
View File

@ -6,9 +6,9 @@
"constructorconsistency.sml" ===> [DONE (force_initialize_attributes still left]
"operationalconsistency.sml" ===> [ready for isabelle]
"refineconstraint.sml" ===> [ready for isabelle]
"commandqueryconsistency.sml" ===> [IMPLEMENTAITON NOT FINISHED]
"taxonomyconsistency.sml" ===> [DONE => works in Isabelle]
"interfaceconsistency.sml" ===> [DONE => works in Isabelle]
"commandqueryconsistency.sml" ===> [ready for isablle (is_modified_only still left)]
"taxonomyconsistency.sml" ===> [DONE]
"interfaceconsistency.sml" ===> [DONE]
"SecureUMLconstraint.sml" ===> [IMPLEMENTATION NOT FINISHED]

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

@ -126,7 +126,7 @@ val wfs = [wfc_vis]
val pos = []
*)
val wfs = []
val wfs = [wfc_quy_strong,wfc_quy_weak]
val pos = [po_rfm_SC]
(*

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

@ -169,6 +169,7 @@ val tax_workaround =
}
val supported_wfs = [
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_inf_stereotypes",
name = "WFC Interface Consistency consistent stereotypes (subconstraint)",
@ -179,6 +180,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.check_stereotypes),
data = Datatab.empty
},
(* SUPPORTED IN ISABELLE *)
WFCPOG.WFPO{
identifier = "wfc_inf_nameclashes",
name = "WFC Interface Consistency no nameclashes (subconstraint)",
@ -189,6 +191,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Interface_Constraint.check_nameclashes),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_inf_all",
name = "WFC Interface Consistency (complete)",
@ -199,6 +202,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(generate_void_wfc),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_vis_class",
name = "WFC Visibility Consistency (class)",
@ -209,6 +213,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Visibility_Constraint.model_entity_consistency),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_vis_inheritance",
name = "WFC Visibility Consistency (inheritance)",
@ -219,6 +224,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Visibility_Constraint.model_inheritance_consistency),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_vis_runtime",
name = "WFC Visibility Consistency (runtime)",
@ -229,6 +235,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Visibility_Constraint.constraint_check_by_runtime_consistency),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_vis_design_by_contract",
name = "WFC Visibility Consistency (design_by_contract)",
@ -239,6 +246,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Visibility_Constraint.constraint_design_by_contract_consistency),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_vis_all",
name = "WFC Visibility Consistency (complete)",
@ -254,6 +262,7 @@ val supported_wfs = [
(* *)
(* (WFCPOG_Taxonomy_Constraint.WFCPOG_TAX_Data.put ({key=9,max_depth=5}) tax_workaround) *)
(* *)
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_tax",
name = "WFC Taxonomy Consistency",
@ -265,6 +274,7 @@ val supported_wfs = [
data = Datatab.empty
}
,
(* NOT SUPPORTED IN ISABLLE (is not needed)*)
WFCPOG.WFPO{
identifier = "wfc_rfm",
name = "WFC OO Refinement",
@ -275,6 +285,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Refine_Constraint.check_syntax),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_cstr_override",
name = "WFC Constructor Consistency",
@ -285,6 +296,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Constructor_Constraint.override_old_creators),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_quy_strong",
name = "WFC Command Query Constraint",
@ -295,6 +307,7 @@ val supported_wfs = [
apply = WFCPOG.WFC(WFCPOG_Command_Query_Constraint.strong_is_query),
data = Datatab.empty
},
(* SUPPORTED IN ISABLLE *)
WFCPOG.WFPO{
identifier = "wfc_quy_weak",
name = "WFC Command Query Constraint",