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

added body to operation 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@6560 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2007-06-07 16:12:25 +00:00
parent 0707f585f9
commit 6e656ff3b1
4 changed files with 174 additions and 161 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

310
src/ocl_library.sml
View File

File diff suppressed because it is too large Load Diff

12
src/rep_core.sml
View File

@ -30,6 +30,7 @@ type Visibility
type operation = { name : string,
precondition : (string option * Rep_OclTerm.OclTerm) list,
postcondition : (string option * Rep_OclTerm.OclTerm) list,
body : (string option * Rep_OclTerm.OclTerm) list,
arguments : (string * Rep_OclType.OclType) list,
result : Rep_OclType.OclType,
isQuery : bool,
@ -127,6 +128,7 @@ val activity_graphs_of: Classifier -> Rep_ActivityGraph.ActivityGraph list
val arguments_of_op : operation -> (string * Rep_OclType.OclType) list
val precondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val body_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val result_of_op : operation -> Rep_OclType.OclType
val postcondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val name_of_op : operation -> string
@ -161,6 +163,7 @@ type Scope = XMI_DataTypes.ScopeKind
type operation = { name : string,
precondition : (string option * Rep_OclTerm.OclTerm) list,
postcondition : (string option * Rep_OclTerm.OclTerm) list,
body : (string option * Rep_OclTerm.OclTerm) list,
arguments : (string * Rep_OclType.OclType) list,
result : Rep_OclType.OclType,
isQuery : bool,
@ -483,14 +486,14 @@ fun update_operations operations' (Class{name,parent,attributes,invariant,operat
fun update_precondition pre' ({name,precondition,postcondition,arguments,result,isQuery,scope,visibility}:operation)
fun update_precondition pre' ({name,precondition,postcondition,body,arguments,result,isQuery,scope,visibility}:operation)
= ({name=name,precondition=pre',postcondition=postcondition,
arguments=arguments,result=result,isQuery=isQuery,scope=scope,
arguments=arguments,body=body,result=result,isQuery=isQuery,scope=scope,
visibility=visibility}:operation)
fun update_postcondition post' ({name,precondition,postcondition,arguments,result,isQuery,scope,visibility}:operation)
fun update_postcondition post' ({name,precondition,postcondition,body,arguments,result,isQuery,scope,visibility}:operation)
= ({name=name,precondition=precondition,postcondition=post',
arguments=arguments,result=result,isQuery=isQuery,scope=scope,
arguments=arguments,body=body,result=result,isQuery=isQuery,scope=scope,
visibility=visibility}:operation)
@ -635,6 +638,7 @@ fun precondition_of_op ({precondition,...}:operation) = case precondition of
[] => [(NONE, Rep_OclTerm.Literal ("true",Rep_OclType.Boolean))]
| il => il
fun body_of_op ({body,...}:operation) = body
fun postcondition_of_op ({postcondition, ...}:operation) = case postcondition of
[] => [(NONE, Rep_OclTerm.Literal ("true",Rep_OclType.Boolean))]

1
src/rep_parser.sml
View File

@ -218,6 +218,7 @@ fun transform_operation t {xmiid,name,isQuery,parameter,visibility,
(find_constraint t))
(filter_bodyconstraint t checked_constraints)],
result = result_type,
body = [],
visibility = visibility,
scope = ownerScope,
isQuery = isQuery (* FIX *)

12
src/rep_su2holocl.sml
View File

@ -87,13 +87,14 @@ fun deep_atpre (t as Literal _) = t
(* FIXME: find appropriate name for this function *)
fun transform_postconds {name, precondition, postcondition, arguments, result,
fun transform_postconds {name, precondition, postcondition, body,arguments, result,
isQuery, scope, visibility} =
{ name=name,
precondition=precondition,
postcondition=map (fn (s,t) => (s,deep_atpre t)) postcondition,
arguments=arguments,
result=result,
body=body,
isQuery=isQuery,
scope=scope,
visibility=visibility
@ -208,6 +209,7 @@ fun replace_attcalls (t as Literal _) = t
fun create_getter c {name,attr_type,visibility,scope,stereotypes,init} =
{ name="get"^(capitalize name),
precondition=nil,
body=nil,
(* post: result=self.att *)
postcondition=[(SOME ("generated_getter_for_"^name),
ocl_eq (result attr_type)
@ -233,6 +235,7 @@ fun create_setter c {name,attr_type,visibility,scope,stereotypes,init} =
in
{ name="set"^(capitalize name),
precondition=nil,
body=nil,
postcondition=[(SOME ("generated_setter_for_"^name),
ocl_and (ocl_eq self_att
(Variable ("arg", attr_type)))
@ -251,7 +254,7 @@ fun create_setter c {name,attr_type,visibility,scope,stereotypes,init} =
* calls to appropriate getter functions, and operation calls with calls
* to corresponding "secured" operations.
*)
fun create_secured {name, precondition, postcondition, arguments, result,
fun create_secured {name, body,precondition, postcondition, arguments, result,
isQuery, scope, visibility} =
{ name=name^"_sec",
precondition=precondition,
@ -259,6 +262,7 @@ fun create_secured {name, precondition, postcondition, arguments, result,
postcondition,
arguments=arguments,
result=result,
body=body,
isQuery=isQuery,
scope=scope,
visibility=public
@ -344,6 +348,7 @@ fun add_operations c =
ocl_and (ocl_isNew (result self_type))
(ocl_modifiedOnly (ocl_set [res] (self_type))))
],
body = [],
arguments=nil,
result=Classifier (name_of c),
isQuery=false,
@ -351,6 +356,7 @@ fun add_operations c =
visibility=public}
val destructor = {name="delete",
precondition=nil,
body=nil,
(* post: self.oclIsUndefined() and self@pre->modifiedOnly() *)
postcondition=[(SOME "generated_destructor",
ocl_and (ocl_isUndefined (self self_type))
@ -394,6 +400,7 @@ val role =
name="getRoleByName",
postcondition=[],
precondition=[],
body=[],
result=Classifier ["AuthorizationEnvironment","Role"],
scope=ClassifierScope,
visibility=public}],
@ -473,6 +480,7 @@ val static_auth_env = [
name="isInRole",
postcondition=[],
precondition=[],
body=[],
result=Boolean,
scope=InstanceScope,
visibility=public}],