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

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

This commit is contained in:
Manuel Krucker 2008-04-23 14:17:56 +00:00
parent 55763cafb9
commit 0c92e2a7da
1 changed files with 17 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
su4sml/src/wfcpog/operational_consistency.sml
View File

@ -43,14 +43,14 @@
signature WFCPOG_OPERATIONAL_CONSTRAINT =
sig
(** sub constraint, included in operational consistency.*)
val generate_secureUML_creators_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_creators_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
(** sub constraint, included in operational consistency.*)
val generate_secureUML_destructors_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_destructors_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
(** sub constraint, included in operational consistency.*)
val generate_secureUML_getters_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_setters_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_op_sec_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_pos : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_getters_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
val generate_secureUML_setters_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
val generate_secureUML_op_sec_po : Rep_Core.Classifier -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
val generate_pos : WFCPOG.wfpo -> Rep.Model -> (string * Rep_OclTerm.OclTerm) list
end
structure WFCPOG_Operational_Constraint : WFCPOG_OPERATIONAL_CONSTRAINT =
@ -149,12 +149,12 @@ fun generate_secureUML_creators_po class (model as (clist,alist)) =
val term1 = OperationCall(result,op_res,(name_of class)@["oclIsUndefined"],[],Boolean)
val term2 = OperationCall(result,op_res,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
(("oper_model_constr"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean))
end
) creators)
end
fun generate_secureUML_destructors_po class (model as (clist,alist)) =
fun generate_secureUML_destructors_po class (model as (clist,alist)) =
let
val destructors = destruction_operations_of class model
in
@ -165,7 +165,7 @@ fun generate_secureUML_destructors_po class (model as (clist,alist)) =
val atPre = OperationCall(self,type_of class,["oclLib","OclAny","atPre"],[],type_of class)
val term2 = OperationCall(atPre,type_of class,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
(("oper_model_destr_"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean))
end
) destructors)
end
@ -182,7 +182,7 @@ fun generate_secureUML_getters_po class (model as (clist,alist)) =
val self = Variable("self",type_of class)
val atCall = AttributeCall(self,type_of class,(name_of class)@[(att_name)],op_res)
in
OperationCall(result,op_res,["oclLib","Boolean","="],[(atCall,op_res)],Boolean)
(("oper_model_getters_"^(string_of_path (name_of class))),OperationCall(result,op_res,["oclLib","Boolean","="],[(atCall,op_res)],Boolean))
end
) getter)
end
@ -201,7 +201,7 @@ fun generate_secureUML_setters_po class (model as (clist,alist)) =
val term1 = OperationCall(att,arg_type,["oclLib","Boolean","="],[(arg,arg_type)],Boolean)
val term2 = OperationCall(att,arg_type,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
(("oper_model_setters_"^(string_of_path (name_of class))),OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean))
end
) setter)
end
@ -213,9 +213,13 @@ fun generate_secureUML_op_sec_po class (model as (clist,alist)) =
List.concat (List.map (fn a =>
let
val real_op = secureUML_real_op a class model
val add_pres = List.map (fn (a,b) => b ) (precondition_of_op real_op)
val add_pres = List.map (fn (a,b) => (case a of
NONE => (("pre_"^(string_of_path(name_of class))),b)
| SOME(x) => (x,b))) (precondition_of_op real_op)
val real_posts = postcondition_of_op real_op
val add_posts = List.map (fn (a,b) => secureUML_substitute_terms b class) (real_posts)
val add_posts = List.map (fn (a,b) => (case a of
NONE => (("post_"^(string_of_path(name_of class))),(secureUML_substitute_terms b class))
| SOME(x) => (x,(secureUML_substitute_terms b class)))) (real_posts)
in
add_pres@add_posts
end