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

merged wfcpo branch changes r6962:7212 into trunk 

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7216 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2008-02-01 10:44:04 +00:00
parent 0bb463a088
commit dbea8f3f0a
35 changed files with 2501 additions and 284 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

331
su4sml/src/ocl_library.sml
View File

File diff suppressed because it is too large Load Diff

98
su4sml/src/ocl_parser/library.sml
View File

@ -43,12 +43,12 @@ signature EXT_LIBRARY =
sig
(* operations with parents *)
val class_of_parent : Rep_Core.Classifier -> Rep_Core.Classifier list -> Rep_Core.Classifier
val class_of_parent : Rep_Core.Classifier -> Rep_Core.transform_model -> Rep_Core.Classifier
val type_of_parent : Rep_Core.Classifier -> Rep_OclType.OclType
val type_of_parents : Rep_Core.Classifier -> Rep_Core.transform_model -> Rep_OclType.OclType list
(* classifiers and packages *)
val class_of_type : Rep_OclType.OclType -> Rep_Core.Classifier list -> Rep_Core.Classifier
val get_classifier : Rep_OclTerm.OclTerm -> Rep_Core.Classifier list -> Rep_Core.Classifier
val class_of_type : Rep_OclType.OclType -> Rep_Core.transform_model -> Rep_Core.Classifier
val get_classifier : Rep_OclTerm.OclTerm -> Rep_Core.transform_model -> Rep_Core.Classifier
val package_of_template_parameter : Rep_OclType.OclType -> string list
(* operations for types *)
@ -95,6 +95,7 @@ sig
val function_calls : int
val function_arguments : int
val zero : int
val exce : int
val high : int
val medium : int
val low : int
@ -110,15 +111,17 @@ sig
exception NoSuchAttributeError of string
exception NoSuchAssociationEndError of string
exception NoSuchOperationError of string
exception NoParentForDatatype of string
end
structure Ext_Library:EXT_LIBRARY =
struct
open Rep
open Rep_Core
open Rep_OclType
open Rep_OclTerm
open OclLibrary
open XMI_DataTypes
exception InterferenceError of string
exception TemplateInstantiationError of string
@ -129,6 +132,7 @@ exception NoCollectionTypeError of OclType
exception NoSuchAttributeError of string
exception NoSuchAssociationEndError of string
exception NoSuchOperationError of string
exception NoParentForDatatype of string
(* Error logging *)
(* default value *)
@ -138,6 +142,7 @@ val log_level = ref 6
val function_calls = 5
val function_arguments = 6
val zero = 0
val exce = 0
val high = 10
val medium = 20
val low = 100
@ -277,6 +282,7 @@ fun type_of_term (Literal (s,typ)) = typ
| type_of_term (OperationWithType (_,_,_,_,res_typ)) = res_typ
| type_of_term (Let (_,_,_,_,_,res_typ)) = res_typ
| type_of_term (Iterate (_,_,_,_,_,_,_,_,res_typ)) = res_typ
| type_of_term (Predicate (_,_,_,_)) = Boolean
fun type_of_CollPart (CollectionItem (term,typ)) = typ
| type_of_CollPart (CollectionRange (term1,term2,typ)) = typ
@ -547,6 +553,7 @@ fun substitute_operations typ [] = []
result = res,
visibility = #visibility oper,
isQuery = #isQuery oper,
stereotypes = #stereotypes oper,
scope = #scope oper
}:operation)::(substitute_operations typ tail)
end
@ -585,7 +592,9 @@ fun substitute_classifier typ classifier =
interfaces = [],
(* a template's thyname is NONE *)
thyname = NONE,
(* a template has no activity_graphs *)
(* a template's visibility is public *)
visibility = public:Rep_Core.Visibility,
(* a template has no activity_graphs *)
activity_graphs = []
})
end
@ -593,32 +602,33 @@ fun substitute_classifier typ classifier =
(* RETURN: Classifer *)
and get_classifier source model =
and get_classifier source (c:Classifier list, a:association list) =
let
val typ = type_of_term (source)
val _ = map (fn a => trace development (string_of_OclType (type_of a) ^"\n") ) model
fun class_of_t typ cl = hd (List.filter (fn a => if ((type_of a) = typ) then true else false) cl)
val _ = map (fn a => trace development (string_of_OclType (type_of a) ^ "\n")) c
fun class_of_t typ m =
hd (List.filter (fn a => if ((type_of a) = typ) then true else false) m)
in
case typ of
(* Primitive types of lib *)
Boolean => class_of_t Boolean model
| Integer => class_of_t Integer model
| Real => class_of_t Real model
| String => class_of_t String model
Boolean => class_of_t Boolean c
| Integer => class_of_t Integer c
| Real => class_of_t Real c
| String => class_of_t String c
(* Template types of lib *)
| Sequence (T) => templ_of (Sequence(TemplateParameter "T")) T model
| Set (T) => templ_of (Set(TemplateParameter "T")) T model
| OrderedSet (T) => templ_of (OrderedSet(TemplateParameter "T")) T model
| Bag (T) => templ_of (Bag(TemplateParameter "T")) T model
| Collection (T) => templ_of (Collection(TemplateParameter "T")) T model
| Sequence (T) => templ_of (Sequence(TemplateParameter "T")) T c
| Set (T) => templ_of (Set(TemplateParameter "T")) T c
| OrderedSet (T) => templ_of (OrderedSet(TemplateParameter "T")) T c
| Bag (T) => templ_of (Bag(TemplateParameter "T")) T c
| Collection (T) => templ_of (Collection(TemplateParameter "T")) T c
(* Class types of lib *)
| OclVoid => class_of_t OclVoid model
| OclAny => class_of_t OclAny model
| OclVoid => class_of_t OclVoid c
| OclAny => class_of_t OclAny c
(* Model types *)
| Classifier (path) =>
let
val _ = trace development ("get_classifier: Classifier ("^(string_of_path path)^")\n")
val res = class_of_t (Classifier (path)) model
val res = class_of_t (Classifier (path)) c
val _ = trace development ("found: "^(string_of_path (name_of res)) ^"\n")
in
(*class_of_t (Classifier (path)) model*)
@ -662,7 +672,7 @@ and templ_of temp_typ para_typ [] = raise TemplateInstantiationError ("Error dur
templ_of temp_typ para_typ tail
end
and class_of_type typ model =
and class_of_type typ (model:Rep_Core.transform_model) =
get_classifier (Variable ("x",typ)) model
(* RETURN: Boolean *)
@ -705,8 +715,8 @@ fun conforms_to_up _ OclAny (_:Rep_Core.transform_model) = true
end
| conforms_to_up typ1 typ2 (model as(classifiers,associations)) =
let
val class = class_of_type typ1 classifiers
val parents_types = type_of_parents (class) classifiers
val class = class_of_type typ1 model
val parents_types = type_of_parents (class) model
val _ = trace low ("conforms_to_up: ... \n")
in
member (typ2) (parents_types)
@ -735,7 +745,7 @@ and upcast (term,typ) =
OperationWithType (term,type_of_term term,"oclIsTypeOf",typ,typ)
(* RETURN: OclType list *)
and type_of_parents (Primitive {parent,...}) model =
and type_of_parents (Primitive {parent,...}) (model:Rep_Core.transform_model) =
(
case parent of
NONE => [OclAny]
@ -762,22 +772,23 @@ and type_of_parents (Primitive {parent,...}) model =
(* RETURN: Classifier *)
fun class_of_parent (Class {parent,...}) clist =
fun class_of_parent (Class {parent,...}) (model:Rep_Core.transform_model) =
(case parent of
NONE => get_classifier (Variable ("x",OclAny)) clist
| SOME (others) => get_classifier (Variable ("x",others)) clist
NONE => get_classifier (Variable ("x",OclAny)) model
| SOME (others) => get_classifier (Variable ("x",others)) model
)
| class_of_parent (AssociationClass {parent,...}) clist =
| class_of_parent (AssociationClass {parent,...}) model =
(case parent of
NONE => get_classifier (Variable ("x",OclAny)) clist
| SOME (others) => get_classifier (Variable ("x",others)) clist
NONE => get_classifier (Variable ("x",OclAny)) model
| SOME (others) => get_classifier (Variable ("x",others)) model
)
| class_of_parent (Primitive {parent,...}) clist =
| class_of_parent (Primitive {parent,...}) model =
(case parent of
NONE => class_of_type OclAny clist
| SOME (others) => class_of_type others clist
NONE => class_of_type OclAny model
| SOME (others) => class_of_type others model
)
| class_of_parent (Interface {parents,...}) clist =
| class_of_parent (Interface {parents,...}) model =
(* TODO: change API *)
(*
(case (List.last (parents)) of
@ -785,9 +796,8 @@ fun class_of_parent (Class {parent,...}) clist =
| SOME (others) => class_of_type others clist
)
*)
class_of_type (List.hd parents) clist
| class_of_parent c (h::tail) = class_of_parent c tail
class_of_type (List.hd parents) model
| class_of_parent c model = raise NoParentForDatatype "No Parent for this type of Classifier"
(* RETURN: Boolean *)
fun args_interfereable [] [] model = true
@ -921,11 +931,11 @@ fun get_overloaded_methods class op_name ([],_) = raise NoModelReferenced ("in '
val _ = trace low("Look for methods for classifier: " ^ string_of_OclType (type_of class) ^ "\n")
val ops2 = List.filter (fn a => (if ((#name a) = op_name) then true else false)) ops
val _ = trace low("operation name : " ^ op_name ^ " Found " ^ Int.toString (List.length ops2) ^ " method(s) \n")
val parent = class_of_parent class classifiers
val parent = class_of_parent class model
val _ = trace low("Parent class : " ^ string_of_OclType (type_of parent) ^ "\n\n")
val cl_op = List.map (fn a => (class,a)) ops2
in
if (class = class_of_type OclAny classifiers)
if (class = class_of_type OclAny model)
then (* end of hierarchie *)
if (List.length ops2 = 0)
then[]
@ -977,7 +987,7 @@ fun get_overloaded_attrs_or_assocends class attr_name ([],_) = raise NoModelRefe
val assocends2 = List.filter (fn {name,...} => (List.last name)=attr_name) assocends
val _ = trace low ("Name of attr/assocend : " ^ attr_name ^ " Found " ^ Int.toString (List.length attrs2) ^
" attribute(s), " ^ Int.toString (List.length assocends2) ^ " assocend(s) \n")
val parent = class_of_parent class classifiers
val parent = class_of_parent class model
val _ = trace low ("Parent class : " ^ string_of_OclType(type_of parent) ^ "\n\n")
val _ = trace low ("Size of attrs2: "^(Int.toString (List.length attrs2))^"\n")
val _ = trace low ("Size of assocends2: "^(Int.toString (List.length assocends2))^"\n")
@ -985,7 +995,7 @@ fun get_overloaded_attrs_or_assocends class attr_name ([],_) = raise NoModelRefe
val cl_as = List.map (fn a => (class,NONE,SOME(a))) assocends2
val _ = trace low ("search done\n")
in
if (class = class_of_type OclAny classifiers) then
if (class = class_of_type OclAny model) then
(* end of hierarchie *)
if (List.length attrs2 = 0)
then if (List.length assocends2 = 0)
@ -1019,7 +1029,7 @@ fun get_meth source op_name args (model as (classifiers,associations))=
(* object type *)
let
val _ = trace low ("Type of Classifier : " ^ string_of_OclType (type_of_term source ) ^ "\n")
val class = get_classifier source classifiers
val class = get_classifier source model
val meth_list = get_overloaded_methods class op_name model
val _ = trace low ("overloaded methods found: " ^ Int.toString (List.length meth_list) ^ "\n")
in
@ -1031,7 +1041,7 @@ fun get_attr_or_assoc source attr_name (model as (classifiers,associations)) =
let
val _ = trace function_calls "get_attr_or_assoc\n"
val _ = trace low ("GET ATTRIBUTES OR ASSOCENDS: source term = " ^ Ocl2String.ocl2string false source ^ "\n")
val class = get_classifier source classifiers
val class = get_classifier source model
val attr_or_assocend_list = get_overloaded_attrs_or_assocends class attr_name model
val _ = trace low ("overloaded attributes/associationends found: " ^ Int.toString (List.length attr_or_assocend_list) ^ "\n")
in

27
su4sml/src/ocl_parser/make_classifier_list.sml
View File

@ -52,7 +52,7 @@ sig
val add_postcondition : string * string option * Rep_OclTerm.OclTerm -> Rep_Core.operation list -> Rep_Core.operation list
val add_body : string * string option * Rep_OclTerm.OclTerm -> Rep_Core.operation list -> Rep_Core.operation list
val add_attribute : string * Rep_OclTerm.OclTerm -> Rep_Core.attribute list -> Rep_Core.attribute list
val context_to_classifier : Context.context -> Rep_Core.Classifier list -> Rep_Core.Classifier
val context_to_classifier : Context.context -> Rep_Core.transform_model -> Rep_Core.Classifier
val merge_classifier : Rep_Core.Classifier -> Rep_Core.Classifier list -> Rep_Core.Classifier list
val gen_updated_classifier_list: (Context.context option) list -> Rep_Core.Classifier list -> Rep_Core.Classifier list
end
@ -87,6 +87,7 @@ fun add_precondition (op_name,cond_name,term) ((oper: operation)::operations_tai
result = #result oper,
isQuery = #isQuery oper,
visibility = #visibility oper,
stereotypes = #stereotypes oper,
scope = #scope oper})
::(operations_tail)
else
@ -102,6 +103,7 @@ fun add_postcondition (op_name,cond_name,term) ((oper: operation)::operations_ta
arguments = #arguments oper,
result = #result oper,
isQuery = #isQuery oper,
stereotypes = #stereotypes oper,
visibility = #visibility oper,
scope = #scope oper})
::(operations_tail)
@ -118,6 +120,7 @@ fun add_body (op_name,cond_name,term) ((oper: operation)::operations_tail) =
arguments = #arguments oper,
result = #result oper,
isQuery = #isQuery oper,
stereotypes = #stereotypes oper,
visibility = #visibility oper,
scope = #scope oper})
::(operations_tail)
@ -172,7 +175,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
in
(
case c of
(Class {name,parent,attributes,operations,associations,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(Class {name,parent,attributes,operations,associations,visibility,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
Class
{
name = name,
@ -184,9 +187,10 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
stereotypes = stereotypes,
invariant = invariant@[(string_opt,term)],
thyname = thyname,
visibility = visibility,
activity_graphs = activity_graphs
}
| (AssociationClass {name,parent,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
| (AssociationClass {name,visibility,parent,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
AssociationClass
{
name = name,
@ -196,6 +200,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
associations = associations,
association = association,
interfaces = interfaces,
visibility = visibility,
stereotypes = stereotypes,
invariant = invariant@[(string_opt,term)],
thyname = thyname,
@ -223,7 +228,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
in
(
case c of
(Class {name,parent,attributes,operations,associations,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(Class {name,parent,attributes,visibility,operations,associations,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(
case attrorassoc of
init =>
@ -235,6 +240,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
associations = associations,
interfaces = interfaces,
stereotypes = stereotypes,
visibility = visibility,
invariant = invariant,
thyname = thyname,
activity_graphs = activity_graphs
@ -242,7 +248,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
| derive => raise NotYetSupportedError ("derive not yet supported ... sorry" ^ "\n")
| def => raise NotYetSupportedError ("def not yet supported ... sorry" ^ "\n")
)
| (AssociationClass {name,parent,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
| (AssociationClass {name,parent,visibility,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(
case attrorassoc of
init =>
@ -252,6 +258,7 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
parent = parent,
attributes = add_attribute (List.last path,term) (attributes),
operations = operations,
visibility = visibility,
associations = associations,
association = association,
interfaces = interfaces,
@ -276,11 +283,12 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
in
(
case c of
(Class {name,parent,attributes,operations,associations,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
(Class {name,parent,attributes,visibility,operations,associations,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
Class
{
name = name,
parent = parent,
visibility = visibility,
attributes = attributes,
operations = add_operations cond_type (op_name,cond_name,term) operations,
associations = associations,
@ -290,11 +298,12 @@ fun context_to_classifier (Inv (path,string_opt,term)) model =
thyname = thyname,
activity_graphs = activity_graphs
}
| (AssociationClass {name,parent,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
| (AssociationClass {name,visibility,parent,attributes,operations,associations,association,interfaces,stereotypes,invariant,thyname,activity_graphs}) =>
AssociationClass
{
name = name,
parent = parent,
visibility = visibility,
attributes = attributes,
operations = add_operations cond_type (op_name,cond_name,term) operations,
associations = associations,
@ -327,13 +336,13 @@ fun merge_classifier classifier (h::classifier_list_tail) =
(classifier)::(classifier_list_tail)
else
(* take next classifier *)
h::(merge_classifier classifier classifier_list_tail)
h::(merge_classifier classifier (classifier_list_tail))
(* RETURN: Classifier list *)
fun gen_updated_classifier_list [] model = model
| gen_updated_classifier_list (SOME(h)::context_list_tail) model =
let
val updated_classifier = context_to_classifier h model
val updated_classifier = context_to_classifier h (model,[])
in
gen_updated_classifier_list context_list_tail (merge_classifier updated_classifier model)
handle AlreadyInitValueError (attr_path,term,mes) =>

1
su4sml/src/ocl_parser/model_import.sml
View File

@ -89,6 +89,7 @@ fun importArgoUMLUnNormalized file =
val model = readFileUnNormalized tmpFile
val _ = OS.FileSys.remove tmpFile
in
model
end

3
su4sml/src/ocl_parser/preprocessor.sml
View File

@ -288,6 +288,7 @@ and generate_variables (Literal (paras)) path meth_name model = Literal (paras)
let
val _ = trace low ("generate_variable: AttributeCall\n")
val _ = List.app (print o (fn x => x^"\n") o string_of_path o name_of ) model
(* val classifier = obsolete_obsolete_class_of path model *)
val classifier = class_of path model
val _ = trace low "classifier found\n"
val meth_list = operations_of classifier
@ -400,7 +401,7 @@ fun preprocess_context (Cond (path,op_name,op_sign,result_type,cond,pre_name,exp
val vexpr = generate_variables expr path op_name model
val _ = trace zero ("Variable 'result' embeded ... \n")
(* embed method arguments *)
val class = class_of_type (Classifier (path)) model
val class = class_of_type (Classifier (path)) (model,[])
val prfx = package_of class
val prefixed_op_sign = List.map (fn (a,b) => (a,prefix_type prfx b)) op_sign
val prefixed_result_type = prefix_type prfx result_type

32
su4sml/src/ocl_parser/type_checker.sml
View File

@ -113,7 +113,7 @@ fun check_argument_type [] [] = true
(* RETURN: OclTerm (OperationCall/AttributeCall) *)
fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs):Rep_Core.transform_model) =
if (attr_or_meth = 0)
then (* OperationCall *)
let
@ -121,7 +121,7 @@ fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
val _ = trace low ("\n==> FromSet-desugarator: operation ... \n")
val new_type = template_parameter (type_of_term rterm)
val iterVar = (("anonIterVar_" ^ (varcounter.nextStr())),new_type)
val class = get_classifier (Variable (iterVar)) cls
val class = get_classifier (Variable (iterVar)) model
val ops = get_overloaded_methods class (List.last path) model
in
if (List.length ops = 0)
@ -140,7 +140,7 @@ fun FromSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
val _ = trace low ("\n==> FromSet-desugarator: attribute/assocend ... \n")
val new_type = template_parameter (type_of_term rterm)
val iterVar = (("anonIterVar_" ^ (varcounter.nextStr())),new_type)
val class = get_classifier (Variable (iterVar)) cls
val class = get_classifier (Variable (iterVar)) model
val attrs_or_assocs = get_overloaded_attrs_or_assocends class (List.last path) model
in
if (List.length attrs_or_assocs = 0)
@ -189,7 +189,7 @@ fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
val _ = trace low ("\n==> AsSet-desugarator: operation ... \n")
val rtyp = Set(type_of_term rterm)
val _ = trace low ("Type of source term " ^ string_of_OclType rtyp ^ " ---> try Set(" ^ string_of_OclType rtyp ^ ")\n")
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),rtyp)) cls
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),rtyp)) model
val ops = get_overloaded_methods class (List.last path) model
val new_rterm = CollectionLiteral([CollectionItem(rterm,type_of_term rterm)],rtyp)
in
@ -204,7 +204,7 @@ fun AsSet_desugarator rterm path attr_or_meth rargs (model as (cls,assocs)) =
val _ = trace low ("\n==> AsSet-desugarator: attribute/assocend\n")
val rtyp = Set(type_of_term rterm)
val _ = trace low (string_of_OclType rtyp ^ "\n")
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),Set(rtyp))) cls
val class = get_classifier (Variable ("anonIterVar_" ^ (varcounter.nextStr()),Set(rtyp))) model
val attrs = get_overloaded_attrs_or_assocends class (List.last path) model
(* source term is a dummy-Term *)
val new_rterm = CollectionLiteral([CollectionItem(rterm,type_of_term rterm)],rtyp)
@ -317,10 +317,10 @@ and resolve_OclTerm (Literal (s,typ)) model =
val rtyp = type_of_term rterm
val _ = trace low (string_of_OclType rtyp ^ "\n")
val templ_type = template_parameter rtyp
val pclass = get_classifier (Variable ("x",templ_type)) cls
val pclass = get_classifier (Variable ("x",templ_type)) model
val ntempl_type = type_of_parent pclass
val new_type = replace_templ_para rtyp ntempl_type
val new_class = get_classifier (Variable ("x",new_type)) cls
val new_class = get_classifier (Variable ("x",new_type)) model
val attrs = get_overloaded_attrs_or_assocends new_class (List.last attr_path) model
val _ = trace low ("parent type of term:" ^ string_of_OclType new_type ^ "\n")
in
@ -349,7 +349,7 @@ let
val _ = trace low ("res OpCall: oclIsTypeOf 3: " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm cls
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
@ -367,7 +367,7 @@ let
val _ = trace low ("res OpCall: oclIsKindOf 3:" ^ "... " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm cls
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
@ -385,7 +385,7 @@ let
val _ = trace low ("res OpCall: oclAsType 3:" ^ "... " ^ "\n")
(* need to prefix the package *)
(* because parameter is written relativly *)
val class = get_classifier rterm cls
val class = get_classifier rterm model
val prfx = package_of class
val _ = trace low ("type of classifier: " ^ string_of_path prfx ^ "\n")
val ctyp = prefix_type prfx (string_to_type [real_typ])
@ -430,11 +430,11 @@ let
val rtyp = type_of_term rterm
val _ = trace low (string_of_OclType rtyp ^ "\n")
val templ_type = template_parameter rtyp
val pclass = get_classifier (Variable ("x",templ_type)) cls
val pclass = get_classifier (Variable ("x",templ_type)) model
val ntempl_type = type_of_parent pclass
val _ = trace low (string_of_OclType ntempl_type ^ "\n")
val new_type = replace_templ_para rtyp ntempl_type
val new_class = get_classifier (Variable ("x",new_type)) cls
val new_class = get_classifier (Variable ("x",new_type)) model
val ops = get_overloaded_methods new_class (List.last meth_path) model
val _ = trace low ("parent type of term: " ^ string_of_OclType new_type ^ "\n")
in
@ -457,7 +457,7 @@ end
val rtyp = type_of_term rterm
val _ = trace low ("res Iter (" ^ name ^ "): source type " ^ string_of_OclType (type_of_term rterm) ^ "\n\n")
(* get source classifier *)
val source_class = get_classifier rterm cls
val source_class = get_classifier rterm model
val _ = trace low ("res Iter (" ^ name ^ "): type of classifier: " ^ string_of_OclType (type_of source_class) ^ "\n")
(* prefix types *)
val prfx = (package_of_template_parameter (type_of source_class))
@ -514,7 +514,7 @@ let
val rtyp = type_of_term rterm
val _ = trace medium ("res Iterate: source type " ^ string_of_OclType (type_of_term rterm) ^ "\n\n")
(* get source classifier *)
val source_class = get_classifier rterm cls
val source_class = get_classifier rterm model
val _ = trace medium ("res Iterate: type of classifier: " ^ string_of_OclType (type_of source_class) ^ "\n")
(* prefix types *)
val prfx = (package_of_template_parameter (type_of source_class))
@ -609,7 +609,7 @@ fun check_context (Cond (path,op_name,op_sign,result_type,cond,pre_name,expr)) (
let
val _ = trace high ("Starts typechecking: ")
val _ = trace high ("pre/post/body : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (path)) cls
val classifier = class_of_type (Classifier (path)) model
val oper_list = operations_of classifier
val oper = find_operation op_name oper_list
val check1 = (op_sign = (#arguments oper))
@ -628,7 +628,7 @@ end
let
val _ = trace high ("Starts typechecking: ")
val _ = trace high ("init/derive : " ^ Ocl2String.ocl2string false expr ^ "\n")
val classifier = class_of_type (Classifier (real_path path)) cls
val classifier = class_of_type (Classifier (real_path path)) model
val _ = trace low ( "classifier found ... " ^ "\n")
val attr_list = attributes_of classifier
val _ = trace low ( "attr_list found ... " ^ "\n")

97
su4sml/src/rep_core.sml
View File

@ -53,6 +53,7 @@ type operation = {
result : Rep_OclType.OclType,
isQuery : bool,
scope : Scope,
stereotypes : string list,
visibility : Visibility
}
@ -94,6 +95,7 @@ datatype Classifier =
stereotypes : string list,
interfaces : Rep_OclType.OclType list,
thyname : string option,
visibility : Visibility,
activity_graphs : Rep_ActivityGraph.ActivityGraph list
}
| AssociationClass of
@ -107,6 +109,7 @@ datatype Classifier =
thyname : string option,
activity_graphs : Rep_ActivityGraph.ActivityGraph list,
associations: Rep_OclType.Path list,
visibility : Visibility,
association: Rep_OclType.Path
}
| Interface (* not supported yet *) of
@ -205,6 +208,10 @@ val addInvariant : constraint -> Classifier -> Classifier
val addInvariants: constraint list -> Classifier -> Classifier
val addOperation : operation -> Classifier -> Classifier
(* visibility *)
val is_visible_cl : Classifier -> bool
val is_visible_op : operation -> bool
val is_visible_attr : attribute -> bool
exception InvalidArguments of string
@ -214,6 +221,7 @@ structure Rep_Core : REP_CORE =
struct
open library
open Rep_OclType
open XMI_DataTypes
type Visibility = XMI_DataTypes.VisibilityKind
type Scope = XMI_DataTypes.ScopeKind
@ -222,13 +230,14 @@ 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,
body : (string option * Rep_OclTerm.OclTerm) list,
arguments : (string * Rep_OclType.OclType) list,
result : Rep_OclType.OclType,
isQuery : bool,
visibility : Visibility,
scope : Scope
}
scope : Scope,
stereotypes : string list,
visibility : Visibility
}
type associationend = {
name : Rep_OclType.Path,
@ -269,6 +278,7 @@ datatype Classifier =
stereotypes : string list,
interfaces : Rep_OclType.OclType list,
thyname : string option,
visibility : Visibility,
activity_graphs : Rep_ActivityGraph.ActivityGraph list
}
| AssociationClass of
@ -282,6 +292,7 @@ datatype Classifier =
thyname : string option,
activity_graphs : Rep_ActivityGraph.ActivityGraph list,
associations: Rep_OclType.Path list,
visibility : Visibility,
association: Rep_OclType.Path
}
| Interface of (* not supported yet *)
@ -491,7 +502,7 @@ fun associationends_of (all_associations:association list)
fun normalize (all_associations:association list)
(C as (Class {name,parent,attributes,operations,associations,
invariant,stereotypes,interfaces,thyname,
activity_graphs})):Classifier =
visibility,activity_graphs})):Classifier =
let
val _ = trace function_calls "normalize: class\n"
val _ = trace function_arguments
@ -516,13 +527,14 @@ fun normalize (all_associations:association list)
stereotypes = stereotypes,
interfaces = interfaces,
thyname = thyname,
visibility = visibility,
activity_graphs = activity_graphs}
end
| normalize all_associations (AC as (AssociationClass
{name,parent,attributes,association,
associations,operations,invariant,
stereotypes,interfaces,
thyname,activity_graphs})) =
thyname,visibility, activity_graphs})) =
(* FIXME: how to handle AssociationClass.association? *)
let
val _ = trace function_calls "normalize: associationclass\n"
@ -546,6 +558,7 @@ fun normalize (all_associations:association list)
thyname = thyname,
activity_graphs = activity_graphs,
associations = [],
visibility=visibility,
association = [] (* FIXME? *)}
end
| normalize all_associations (Primitive p) =
@ -561,6 +574,7 @@ fun normalize (all_associations:association list)
stereotypes = (#stereotypes p),
interfaces = (#interfaces p),
thyname = (#thyname p),
visibility = public,
activity_graphs=[]})
| normalize all_associations c = c
@ -610,7 +624,7 @@ fun init_to_inv cls_name (attr:attribute) =
fun normalize_init (Class {name,parent,attributes,operations,
associations,invariant,
stereotypes,interfaces,thyname,activity_graphs}) =
stereotypes,interfaces,thyname,visibility,activity_graphs}) =
Class {name = name,
parent = parent,
attributes = (map rm_init_attr attributes),
@ -622,11 +636,12 @@ fun normalize_init (Class {name,parent,attributes,operations,
stereotypes = stereotypes,
interfaces = interfaces,
thyname = thyname,
visibility=visibility,
activity_graphs=activity_graphs}
| normalize_init (AssociationClass {name,parent,attributes,operations,
associations,association,
invariant,stereotypes,interfaces,
thyname,activity_graphs}) =
thyname,visibility,activity_graphs}) =
AssociationClass {name = name,
parent = parent,
attributes = (map rm_init_attr attributes),
@ -638,6 +653,7 @@ fun normalize_init (Class {name,parent,attributes,operations,
attributes) invariant,
stereotypes = stereotypes,
interfaces = interfaces,
visibility=visibility,
thyname = thyname,
activity_graphs=activity_graphs}
| normalize_init c = c
@ -649,11 +665,13 @@ val OclAnyC = Class{name=Rep_OclType.OclAny,parent=NONE,attributes=[],
operations=[], interfaces=[],
invariant=[],stereotypes=[], associations=[],
thyname=NONE,
visibility = public,
activity_graphs=nil}
val OclAnyAC = AssociationClass{name=Rep_OclType.OclAny,parent=NONE,
attributes=[],operations=[], interfaces=[],
invariant=[],stereotypes=[], associations=[],
visibility = public,
association= []:Path (*FIXME: sensible dummy*),
thyname=NONE, activity_graphs=nil}
@ -665,7 +683,7 @@ fun string_of_path (path:Rep_OclType.Path) =
fun update_thyname tname (Class{name,parent,attributes,operations,invariant,
stereotypes,interfaces,associations,
activity_graphs,...}) =
visibility,activity_graphs,...}) =
Class{name=name,
parent=parent,
attributes=attributes,
@ -675,11 +693,12 @@ fun update_thyname tname (Class{name,parent,attributes,operations,invariant,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=(SOME tname),
visibility=visibility,
activity_graphs=activity_graphs }
| update_thyname tname (AssociationClass{name,parent,attributes,operations,
invariant,stereotypes,interfaces,
associations,association,
activity_graphs,...}) =
visibility,activity_graphs,...}) =
AssociationClass{name=name,
parent=parent,
attributes=attributes,
@ -690,6 +709,7 @@ fun update_thyname tname (Class{name,parent,attributes,operations,invariant,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=(SOME tname),
visibility=visibility,
activity_graphs=activity_graphs }
| update_thyname tname (Interface{name,parents,operations,stereotypes,
invariant,...}) =
@ -724,7 +744,7 @@ fun update_thyname tname (Class{name,parent,attributes,operations,invariant,
fun update_invariant invariant' (Class{name,parent,attributes,operations,
invariant,stereotypes,interfaces,
associations,activity_graphs,thyname}) =
associations,visibility,activity_graphs,thyname}) =
Class{name=name,
parent=parent,
attributes=attributes,
@ -734,12 +754,13 @@ fun update_invariant invariant' (Class{name,parent,attributes,operations,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=thyname,
visibility=visibility,
activity_graphs=activity_graphs }
| update_invariant invariant' (AssociationClass{name,parent,attributes,
operations,invariant,
stereotypes,interfaces,
association,associations,
activity_graphs,thyname}) =
visibility,activity_graphs,thyname}) =
AssociationClass{name=name,
parent=parent,
attributes=attributes,
@ -750,6 +771,7 @@ fun update_invariant invariant' (Class{name,parent,attributes,operations,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=thyname,
visibility=visibility,
activity_graphs=activity_graphs }
| update_invariant invariant' (Interface{name,parents,operations,stereotypes,
invariant,thyname}) =
@ -788,7 +810,7 @@ fun update_invariant invariant' (Class{name,parent,attributes,operations,
fun update_operations operations' (Class{name,parent,attributes,invariant,
operations,stereotypes,interfaces,
associations,activity_graphs,
thyname}) =
visibility,thyname}) =
Class{name=name,
parent=parent,
attributes=attributes,
@ -797,12 +819,14 @@ fun update_operations operations' (Class{name,parent,attributes,invariant,
operations=operations',
stereotypes=stereotypes,
interfaces=interfaces,
visibility=visibility,
thyname=thyname,
activity_graphs=activity_graphs }
| update_operations operations' (AssociationClass{name,parent,attributes,
invariant,operations,
stereotypes,interfaces,
associations,association,
visibility,
activity_graphs,thyname}) =
AssociationClass{name=name,
parent=parent,
@ -813,6 +837,7 @@ fun update_operations operations' (Class{name,parent,attributes,invariant,
operations=operations',
stereotypes=stereotypes,
interfaces=interfaces,
visibility=visibility,
thyname=thyname,
activity_graphs=activity_graphs }
| update_operations operations' (Interface{name,parents,invariant,
@ -850,7 +875,7 @@ fun update_operations operations' (Class{name,parent,attributes,invariant,
fun update_precondition pre' ({name,precondition,postcondition,body,arguments,
result,isQuery,scope,visibility}:operation) =
result,isQuery,scope,stereotypes,visibility}:operation) =
{name=name,
precondition=pre',
postcondition=postcondition,
@ -859,11 +884,12 @@ fun update_precondition pre' ({name,precondition,postcondition,body,arguments,
result=result,
isQuery=isQuery,
scope=scope,
visibility=visibility}:operation
visibility=visibility,
stereotypes=stereotypes}:operation
fun update_postcondition post' ({name,precondition,postcondition,body,
arguments,result,isQuery,scope,
visibility}:operation) =
stereotypes, visibility}:operation) =
{name=name,
precondition=precondition,
postcondition=post',
@ -872,7 +898,8 @@ fun update_postcondition post' ({name,precondition,postcondition,body,
result=result,
isQuery=isQuery,
scope=scope,
visibility=visibility}:operation
visibility=visibility,
stereotypes=stereotypes}:operation
@ -1126,6 +1153,19 @@ fun operation_of cl fq_name =
then true else false ) operations ))
end
fun is_visible_cl (Class {visibility,...}) =
if (visibility = public) then true else false
| is_visible_cl (AssociationClass {visibility,...}) =
if (visibility = public) then true else false
| is_visible_cl x = true
fun is_visible_op ({visibility,...}:operation) =
if (visibility = public) then true else false
fun is_visible_attr ({visibility,...}:attribute) =
if (visibility = public) then true else false
(* topological sort of class lists *)
fun topsort_cl cl =
let
@ -1185,22 +1225,23 @@ fun connected_classifiers_of (all_associations:association list)
*)
fun addInvariant inv (Class {name, parent, attributes, operations,
associations, invariant, stereotypes,
interfaces, thyname, activity_graphs}) =
interfaces, thyname, visibility,
activity_graphs}) =
Class {name=name, parent=parent, attributes=attributes,
operations=operations,
associations=associations, invariant=inv::invariant,
stereotypes=stereotypes, interfaces=interfaces,
thyname=thyname, activity_graphs=activity_graphs}
thyname=thyname, visibility=visibility,activity_graphs=activity_graphs}
| addInvariant inv (AssociationClass {name, parent, attributes,
operations, associations,
association, invariant,
stereotypes, interfaces,
thyname, activity_graphs}) =
thyname, visibility,activity_graphs}) =
AssociationClass {name=name, parent=parent, attributes=attributes,
operations=operations, associations=associations,
association=association, invariant=inv::invariant,
stereotypes=stereotypes, interfaces=interfaces,
thyname=thyname, activity_graphs=activity_graphs}
thyname=thyname, visibility=visibility,activity_graphs=activity_graphs}
| addInvariant inv (Interface {name, parents, operations,
invariant, stereotypes, thyname}) =
Interface {name=name, parents=parents, operations=operations,
@ -1226,7 +1267,7 @@ fun addInvariant inv (Class {name, parent, attributes, operations,
fun addInvariants invs (Class {name, parent, attributes, operations,
associations, invariant, stereotypes,
interfaces, thyname, activity_graphs}) =
interfaces, thyname, visibility,activity_graphs}) =
Class {name=name,
parent=parent,
attributes=attributes,
@ -1234,6 +1275,7 @@ fun addInvariants invs (Class {name, parent, attributes, operations,
associations=associations,
invariant=invs@invariant,
stereotypes=stereotypes,
visibility=visibility,
interfaces=interfaces,
thyname=thyname,
activity_graphs=activity_graphs}
@ -1241,7 +1283,7 @@ fun addInvariants invs (Class {name, parent, attributes, operations,
operations, associations,
association, invariant,
stereotypes, interfaces,
thyname, activity_graphs}) =
thyname, visibility, activity_graphs}) =
AssociationClass {name=name,
parent=parent,
attributes=attributes,
@ -1250,6 +1292,7 @@ fun addInvariants invs (Class {name, parent, attributes, operations,
association=association,
invariant=invs@invariant,
stereotypes=stereotypes,
visibility=visibility,
interfaces=interfaces,
thyname=thyname,
activity_graphs=activity_graphs}
@ -1290,21 +1333,23 @@ fun addInvariants invs (Class {name, parent, attributes, operations,
(** adds an operation to a classifier. *)
fun addOperation oper (Class {name, parent, attributes, operations,
associations, invariant, stereotypes,
interfaces, thyname, activity_graphs})
interfaces, thyname, visibility,activity_graphs})
= Class {name=name, parent=parent, attributes=attributes,
operations=oper::operations,
associations=associations, invariant=invariant,
stereotypes=stereotypes, interfaces=interfaces,
visibility=visibility,
thyname=thyname, activity_graphs=activity_graphs}
| addOperation oper (AssociationClass {name, parent, attributes,
operations, associations,
association, invariant,
stereotypes, interfaces,
thyname, activity_graphs})
thyname, visibility,activity_graphs})
= AssociationClass {name=name, parent=parent, attributes=attributes,
operations=oper::operations, associations=associations,
association=association, invariant=invariant,
stereotypes=stereotypes, interfaces=interfaces,
stereotypes=stereotypes, interfaces=interfaces,
visibility=visibility,
thyname=thyname, activity_graphs=activity_graphs}
| addOperation oper (Interface {name, parents, operations,
invariant, stereotypes, thyname})

6
su4sml/src/rep_ocl.sml
View File

@ -89,6 +89,9 @@ datatype OclTerm =
| OperationWithType of OclTerm * OclType (* source *)
* string * OclType(* type parameter *)
* OclType (* result type *)
| Predicate of OclTerm * OclType (* source *)
* Path (* name *)
* (OclTerm * OclType) list (* arguments *)
| Variable of string * OclType (* name with type *)
| Let of string * OclType (* variable *)
* OclTerm * OclType (* rhs *)
@ -207,6 +210,9 @@ datatype OclTerm =
| OperationWithType of OclTerm * OclType (* source *)
* string * OclType (* type parameter *)
* OclType (* result type *)
| Predicate of OclTerm * OclType (* source *)
* Path (* name *)
* (OclTerm * OclType) list (* arguments *)
| Variable of string * OclType (* name with type *)
| Let of string * OclType (* variable *)
* OclTerm * OclType (* rhs *)

3
su4sml/src/rep_parser.sml
View File

@ -267,6 +267,7 @@ fun transform_operation t {xmiid,name,isQuery,parameter,visibility,
result = result_type,
body = [],
visibility = visibility,
stereotypes = [], (* FIX *)
scope = ownerScope,
isQuery = isQuery (* FIX *)
}
@ -438,6 +439,7 @@ fun transform_classifier t (XMI.Class {xmiid,name,isActive,visibility,isLeaf,
associations = assocs,
stereotypes = map (find_stereotype t) stereotype,
interfaces = nil, (* FIX *)
visibility = visibility:Rep_Core.Visibility,
activity_graphs = List.concat [map (transform_activitygraph t) activity_graphs,
map (transform_statemachine t) state_machines],
thyname = NONE}
@ -477,6 +479,7 @@ fun transform_classifier t (XMI.Class {xmiid,name,isActive,visibility,isLeaf,
thyname = NONE,
activity_graphs = [] (* FIXME *),
associations = assocs,
visibility = visibility,
association = assoc}
end

36
su4sml/src/rep_su2holocl.sml
View File

@ -229,7 +229,8 @@ fun create_getter c {name,attr_type,visibility,scope,stereotypes,init} =
result=attr_type,
isQuery=true,
scope=scope,
visibility=public
visibility=public,
stereotypes=[]
}
(** creates a setter function for the given attribute.
@ -254,7 +255,8 @@ fun create_setter c {name,attr_type,visibility,scope,stereotypes,init} =
result=OclVoid,
isQuery=false,
scope=scope,
visibility=public
visibility=public,
stereotypes=[]
}
end
@ -264,7 +266,7 @@ fun create_setter c {name,attr_type,visibility,scope,stereotypes,init} =
* to corresponding "secured" operations.
*)
fun create_secured {name, body,precondition, postcondition, arguments, result,
isQuery, scope, visibility} =
isQuery, scope,stereotypes,visibility} =
{ name=name^"_sec",
precondition=precondition,
postcondition=map (fn (name,t) => (name,replace_attcalls (replace_opcalls t)))
@ -274,7 +276,8 @@ fun create_secured {name, body,precondition, postcondition, arguments, result,
body=body,
isQuery=isQuery,
scope=scope,
visibility=public
stereotypes=stereotypes,
visibility=visibility
}
@ -300,7 +303,8 @@ fun add_operations c =
result=Classifier (name_of c),
isQuery=false,
scope=ClassifierScope,
visibility=public}
visibility=public,
stereotypes=[]}
val destructor =
{name="delete",
precondition=nil,
@ -316,7 +320,8 @@ fun add_operations c =
result=OclVoid,
isQuery=false,
scope=InstanceScope,
visibility=public}
visibility=public,
stereotypes=[]}
val getters = map (create_getter c) (attributes_of c)
val setters = map (create_setter c) (attributes_of c)
val sec_ops = map create_secured (operations_of c)
@ -396,7 +401,8 @@ val role =
init=NONE,name="name",
scope=InstanceScope,
stereotypes=[],
visibility=public}],
visibility=public
}],
interfaces=[],
invariant=[],
name=Classifier ["AuthorizationEnvironment","Role"],
@ -408,10 +414,13 @@ val role =
body=[],
result=Classifier ["AuthorizationEnvironment","Role"],
scope=ClassifierScope,
visibility=public}],
stereotypes=[],
visibility=public}
],
parent=NONE,
stereotypes=[],
thyname=NONE}
thyname=NONE,
visibility=public}
val identity =
Class { activity_graphs=[],
@ -441,6 +450,7 @@ val identity =
name=Classifier ["AuthorizationEnvironment","Identity"],
operations=[],
parent=NONE,
visibility=public,
stereotypes=[],
thyname=NONE
}
@ -461,6 +471,7 @@ val static_auth_env = [
name=Classifier ["AuthorizationEnvironment","Context"],
operations=[],
parent=NONE,
visibility=public:Rep_Core.Visibility,
stereotypes=[],
thyname=NONE},
Class
@ -493,13 +504,14 @@ val static_auth_env = [
precondition=[],
body=[],
result=Boolean,
scope=InstanceScope,
visibility=public}],
stereotypes=[],
scope=InstanceScope:Rep_Core.Scope,
visibility=public:Rep_Core.Visibility }],
parent=NONE,
visibility=public:Rep_Core.Visibility,
stereotypes=[],
thyname=NONE}]
(** defines the role hierarchy. *)
(* FIXME: context Identity inv: self.roles.name->includes(r1) implies *)
(* self.roles.name->includes(r2) *)

3
su4sml/src/rep_transform.sml
View File

@ -282,7 +282,7 @@ fun transformAssociationClassIntoClass (AssociationClass
{name,parent,attributes,operations,
associations,association,
invariant,stereotypes,interfaces,
thyname,activity_graphs}) =
visibility,thyname,activity_graphs}) =
Class { name = name,
parent = parent,
attributes = attributes,
@ -292,6 +292,7 @@ fun transformAssociationClassIntoClass (AssociationClass
stereotypes = stereotypes,
interfaces = interfaces,
thyname = thyname,
visibility = visibility,
activity_graphs = activity_graphs}
(**

24
su4sml/src/secure_uml.sml
View File

@ -245,17 +245,18 @@ fun update_aends (Rep.Class { name, parent,attributes,operations,associations,
end
*)
fun update_assocs (Rep.Class { name, parent,attributes,operations,associations,
invariant, stereotypes,interfaces,thyname,activity_graphs}) assocs =
invariant,stereotypes,interfaces,thyname,visibility,activity_graphs}) assocs =
Rep.Class {name=name, parent=parent, attributes=attributes,
operations=operations, associations=assocs,
invariant=invariant, stereotypes=stereotypes,
interfaces=interfaces, thyname=thyname,
visibility=visibility,
activity_graphs=activity_graphs}
| update_assocs (Rep.AssociationClass { name, parent,attributes,operations,associations,association,
invariant, stereotypes,interfaces,thyname,activity_graphs}) assocs =
invariant, stereotypes,interfaces,thyname,visibility,activity_graphs}) assocs =
Rep.AssociationClass {name=name, parent=parent, attributes=attributes,
operations=operations, associations=assocs,association=association,
invariant=invariant, stereotypes=stereotypes,
invariant=invariant, stereotypes=stereotypes,visibility=visibility,
interfaces=interfaces, thyname=thyname,
activity_graphs=activity_graphs}
@ -321,12 +322,10 @@ fun parse (model as (cs,assocs):Rep.Model) =
(* remove classes with SecureUML stereotypes from the association list
* and update affected classes if the association ceases to exist
*)
fun updateClassifierAssociations rem_assocs (Rep.Class
{name,parent,attributes,
operations,associations,
invariant, stereotypes,
interfaces, thyname,
activity_graphs}) =
fun updateClassifierAssociations rem_assocs (Rep.Class {name, parent, attributes, operations,
associations, invariant, stereotypes,
interfaces, thyname,visibility,activity_graphs}) =
let
val assoc_names = map (fn {name,aends,qualifiers,aclass} => name)
rem_assocs
@ -342,11 +341,13 @@ fun parse (model as (cs,assocs):Rep.Model) =
stereotypes = stereotypes,
interfaces = interfaces,
thyname = thyname,
visibility = visibility,
activity_graphs = activity_graphs}
end
| updateClassifierAssociations rem_assocs (Rep.AssociationClass {name, parent, attributes,
operations, associations,
association, invariant,
association, invariant,visibility,
stereotypes, interfaces,
thyname, activity_graphs}) =
let
@ -364,10 +365,11 @@ fun parse (model as (cs,assocs):Rep.Model) =
invariant = invariant,
stereotypes = stereotypes,
interfaces = interfaces,
visibility = visibility,
thyname = thyname,
activity_graphs = activity_graphs
}
end
end
val (modified_assocs,removed_assocs) =
(case secureumlstereotypes of

22
su4sml/src/transform_library.sml
View File

@ -332,13 +332,14 @@ fun name_of_attribute ({name,...}:attribute) = name
fun addAttributes (Class {name,parent,attributes,operations,associations,
invariant,stereotypes,interfaces,thyname,
activity_graphs}) newAttributes =
activity_graphs,visibility}) newAttributes =
Class {name=name,
parent=parent,
attributes=newAttributes@attributes,
operations=operations,
associations=associations,
invariant=invariant,
visibility=visibility,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=thyname,
@ -346,7 +347,7 @@ fun addAttributes (Class {name,parent,attributes,operations,associations,
| addAttributes (AssociationClass {name,parent,attributes,operations,
associations,association,invariant,
stereotypes,interfaces,thyname,
activity_graphs}) newAttributes =
visibility,activity_graphs}) newAttributes =
AssociationClass {name=name,
parent=parent,
attributes=newAttributes@attributes,
@ -357,6 +358,7 @@ fun addAttributes (Class {name,parent,attributes,operations,associations,
stereotypes=stereotypes,
interfaces=interfaces,
thyname=thyname,
visibility=visibility,
activity_graphs=activity_graphs}
| addAttributes (Template {parameter,classifier}) newAttributes=
Template {parameter=parameter,
@ -400,7 +402,8 @@ fun newDummyClass package =
associations=[],
invariant=[],
stereotypes=[],
interfaces=[],
visibility=XMI.private,
interfaces=[],
thyname=NONE,
activity_graphs=[]}
@ -410,6 +413,7 @@ fun newNamedClass package name =
attributes=[],
operations=[],
associations=[],
visibility=XMI.private,
invariant=[],
stereotypes=[],
interfaces=[],
@ -533,11 +537,12 @@ fun updateAssociationReferences classifiers [] = classifiers
operations,associations,
invariant,stereotypes,
interfaces,thyname,
activity_graphs}) =
visibility,activity_graphs}) =
Class{name=name,
parent=parent,
attributes=attributes,
operations=operations,
visibility=visibility,
associations= associations,
invariant=map (handleConstraint oldAssoc newAssocs) invariant,
stereotypes=stereotypes,
@ -549,11 +554,12 @@ fun updateAssociationReferences classifiers [] = classifiers
operations,associations,
invariant,association,
stereotypes,interfaces,
thyname,activity_graphs}) =
visibility,thyname,activity_graphs}) =
AssociationClass{name=name,
parent=parent,
attributes=attributes,
operations=operations,
visibility=visibility,
associations= associations,
association=association,
invariant=map (handleConstraint oldAssoc newAssocs)
@ -674,7 +680,7 @@ fun modifyAssociationsOfClassifier (newAssociations:association list)
(Class{name,parent,attributes,
operations,associations,invariant,
stereotypes,interfaces,thyname,
activity_graphs}) =
visibility,activity_graphs}) =
Class{name=name,
parent=parent,
attributes=attributes,
@ -686,6 +692,7 @@ fun modifyAssociationsOfClassifier (newAssociations:association list)
associations),
invariant=invariant,
stereotypes=stereotypes,
visibility=visibility,
interfaces=interfaces,
thyname=thyname,
activity_graphs=activity_graphs}
@ -694,7 +701,7 @@ fun modifyAssociationsOfClassifier (newAssociations:association list)
operations,associations,
invariant,association,
stereotypes,interfaces,
thyname,activity_graphs}) =
visibility,thyname,activity_graphs}) =
AssociationClass{name=name,
parent=parent,
attributes=attributes,
@ -709,6 +716,7 @@ fun modifyAssociationsOfClassifier (newAssociations:association list)
stereotypes=stereotypes,
interfaces=interfaces,
thyname=thyname,
visibility=visibility,
activity_graphs=activity_graphs}
| modifyAssociationsOfClassifier newAssociations oldAssociations

64
su4sml/src/wfcpo-gen/base_constraint.sml Normal file
View File

@ -0,0 +1,64 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
signature BASE_CONSTRAINT =
sig
include CONSTRAINT
val generate_po : Rep.Model -> Rep_OclTerm.OclTerm list
exception BaseConstraintError of string
end
(** The common properties of a constraint. *)
structure Base_Constraint : BASE_CONSTRAINT =
struct
open Rep_OclTerm
exception SyntaxError of string
exception ConstraintError of string
exception BaseConstraintError of string
type constraint = Constraint.constraint
fun generate_po model = raise BaseConstraintError ("Not possible to apply Base_Constraint.\n")
end

17
su4sml/src/wfcpo-gen/configs/.bash_aliases Normal file
View File

@ -0,0 +1,17 @@
if [ "$TERM" != "dumb" ]; then
eval "`dircolors -b`"
alias ls='ls --color=auto'
fi
alias pg='ps ax | grep '
alias kp='sudo kill -9 '
alias nb='nano ~/.bashrc'
alias fr='sudo find / -name '
alias vpn='sudo vpnc ethz'
alias cs='cd $SU4SML_HOME'
alias cw='cd $WFCPO_HOME'
alias su4sml='cd $HOME/ethz/masterthesis/wf-check_and_po-generation/su4sml'
alias wfcpo='cd $HOME/ethz/masterthesis/wf-check_and_po-generation/su4sml/src/wfcpo-gen'
alias exam='cd $HOME/ethz/masterthesis/wf-check_and_po-generation/examples'

112
su4sml/src/wfcpo-gen/configs/.bashrc Normal file
View File

@ -0,0 +1,112 @@
# ~/.bashrc: executed by bash(1) for non-login shells.
# see /usr/share/doc/bash/examples/startup-files (in the package bash-doc)
# for examples
# If not running interactively, don't do anything
[ -z "$PS1" ] && return
# don't put duplicate lines in the history. See bash(1) for more options
export HISTCONTROL=ignoredups
# gerneral variables
export PATH=$PATH:"/usr/lib/jvm/java-1.5.0-sun-1.5.0.08/bin/"
export CLASSPATH=$CLASSPATH:"/opt/tinyos-2.x/support/sdk/java/tinyos.jar"
# JAVA variables
export JAVA_HOME="/usr/lib/jvm/java-1.5.0-sun-1.5.0.08/"
# CRUISECONTROL variables
export CC_HOME="/home/joe/software/cruisecontrol"
export CC_PRO="$CC_HOME/cruisecontrol-bin-2.7.1/projects"
export CC_WSN="$CC_PRO/manu_wsntest"
# TINYOS variables
export TOSROOT="/opt/tinyos-2.x"
export TOSDIR="$TOSROOT/tos"
export MAKERULES="$TOSROOT/support/make/Makerules"
export PYTHONPATH="/opt/tinyos-2.x/support/sdk/python/"
# DNS variables
export DSNUSER="btnode"
export DSNPASS="btadmin"
export DSNSRV="192.168.110.13"
export DSNPORT="8887"
export TINY_APP_PATH="$CC_WSN/"
#export TEST_TOPOLOGY="inss_topo"
export DSNROOTNODE="00:04:3f:00:01:ae"
export TOSSIMROOTNODE="30"
export TCL_LIBRARY="/usr/lib/tcl8.4"
export TK_LIBRARY="/usr/lib/tk8.4"
# SU4SML variables
export SU4SML_HOME="$HOME/ethz/masterthesis/wf-check_and_po-generation/su4sml"
export WFCPO_HOME="$SU4SML_HOME/src/wfcpo-gen"
# check the window size after each command and, if necessary,
# update the values of LINES and COLUMNS.
shopt -s checkwinsize
# make less more friendly for non-text input files, see lesspipe(1)
[ -x /usr/bin/lesspipe ] && eval "$(lesspipe)"
# set variable identifying the chroot you work in (used in the prompt below)
if [ -z "$debian_chroot" ] && [ -r /etc/debian_chroot ]; then
debian_chroot=$(cat /etc/debian_chroot)
fi
# set a fancy prompt (non-color, unless we know we "want" color)
case "$TERM" in
xterm-color)
PS1='${debian_chroot:+($debian_chroot)}\[\033[01;32m\]\u@\h\[\033[00m\]:\[\033[01;34m\]\w\[\033[00m\]\$ '
;;
*)
PS1='${debian_chroot:+($debian_chroot)}\u@\h:\w\$ '
;;
esac
# Comment in the above and uncomment this below for a color prompt
#PS1='${debian_chroot:+($debian_chroot)}\[\033[01;32m\]\u@\h\[\033[00m\]:\[\033[01;34m\]\w\[\033[00m\]\$ '
# If this is an xterm set the title to user@host:dir
case "$TERM" in
xterm*|rxvt*)
PROMPT_COMMAND='echo -ne "\033]0;${USER}@${HOSTNAME}: ${PWD/$HOME/~}\007"'
;;
*)
;;
esac
# Alias definitions.
# You may want to put all your additions into a separate file like
# ~/.bash_aliases, instead of adding them here directly.
# See /usr/share/doc/bash-doc/examples in the bash-doc package.
if [ -f ~/.bash_aliases ]; then
. ~/.bash_aliases
fi
# enable color support of ls and also add handy aliases
#if [ "$TERM" != "dumb" ]; then
# eval "`dircolors -b`"
# alias ls='ls --color=auto'
#alias dir='ls --color=auto --format=vertical'
#alias vdir='ls --color=auto --format=long'
# fi
# some more ls aliases
#alias ll='ls -l'
#alias la='ls -A'
#alias l='ls -CF'
# enable programmable completion features (you don't need to enable
# this, if it's already enabled in /etc/bash.bashrc and /etc/profile
# sources /etc/bash.bashrc).
if [ -f /etc/bash_completion ]; then
. /etc/bash_completion
fi
# Set up TinyOS environment according to
# http://5secondfuse.com/tinyos/install.html
if [ -f ~/.bash_tinyos ]; then
. ~/.bash_tinyos
fi

29
su4sml/src/wfcpo-gen/constraint.sml Normal file
View File

@ -0,0 +1,29 @@
(** A syntactic or semantic constraint for a UML/OCL model.
* Every constraint consists of at leas a Constraint and Constraint info.
*
*)
signature CONSTRAINT =
sig
type constraint = { name : string,
description : string,
generator : Rep.Model -> Rep_OclTerm.OclTerm list }
exception ConstraintError of string
end
(** The common type for every constraint *)
structure Constraint : CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep
open Rep_OclTerm
type constraint = { name : string,
description : string,
generator : Rep.Model -> OclTerm list }
exception ConstraintError of string
end;

126
su4sml/src/wfcpo-gen/constructor_consistency.sml Normal file
View File

@ -0,0 +1,126 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(** Implementation of the wellformed constraint for a constructor *)
signature CONSTRUCTOR_CONSTRAINT =
sig
include BASE_CONSTRAINT
(** sub constraint, included in constructor consistency.*)
val post_implies_invariant : Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Constructor_Constraint (SuperCon : BASE_CONSTRAINT) : CONSTRUCTOR_CONSTRAINT =
struct
(* SU4SML *)
open Rep_Core
open Rep
open Rep_OclTerm
open Rep_OclType
(* OclParser *)
open Ext_Library
open ModelImport
(* WFCPO *)
open WFCPO_Naming
open WFCPO_Library
exception ConstraintError of string
exception BaseConstraintError of string
exception ConstructorError of string
type constraint = Constraint.constraint
(* Make a string case insensitive *)
fun to_lower_string "" = ""
| to_lower_string s:string =
let
fun to_lower [x] = [Char.toLower x]
| to_lower (h::tail) = (Char.toLower h)::(to_lower tail)
in
String.implode (to_lower (String.explode s))
end
fun generate_return_value crea_op classifier model =
let
(* wrap invariants *)
val invariants = all_invariants_of classifier model
val self_type = type_of classifier
val self_arg = Variable ("self",self_type)
val invs = List.map (fn (a,b) => wrap_predicate b a [(self_arg,self_type)]) invariants
val final_inv = conjugate_terms invs
(* wrap postconditions *)
val sig_args = arguments_of_op crea_op
val args = (self_arg,self_type)::(List.map (fn (a,b) => (Variable(a,b),b)) sig_args)
val postconditions = postcondition_of_op crea_op
val posts = List.map (fn (a,b) => wrap_predicate b a args) postconditions
val final_post = conjugate_terms posts
in
OperationCall(final_post,Boolean,["Boolean","implies"],[(final_inv,type_of_term final_inv)],Boolean)
end
fun post_implies_invariant_help [] model = []
| post_implies_invariant_help (h::class) (model as (clist,alist)) =
let
val crea_ops = creation_operations_of (name_of h) model
val pos = List.map (fn a => generate_return_value a h model) crea_ops
in
pos@(post_implies_invariant_help (class) model)
end
fun post_implies_invariant (model as (clist, alist)) =
let
val class = removeOclLibrary clist
in
post_implies_invariant_help class model
end
fun generate_po (model as (clist,alist)) =
let
val x1 = post_implies_invariant model
in
x1
end
end;

64
su4sml/src/wfcpo-gen/core.sml Normal file
View File

@ -0,0 +1,64 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(**
* The core provides the basic data structures and general exceptions.
*)
signature WFCPO_GEN =
sig
val generate : Rep.Model -> (Rep_OclTerm.OclTerm * string) list
end
functor WFCPO_Gen(C: BASE_CONSTRAINT) : WFCPO_GEN =
struct
open Rep_Core
open Rep
open Rep2String
fun generate model = C.generate_po model
(*fun print_cinfo (LiskovInfo {package,po_producer,po_causer,operation_name,pre_or_post}) =
print("PACKAGE: " ^ (String.concat package) ^ ", SUBCLASS: " ^ (String.concat (name_of po_producer)) ^ ", SUPER_CLASS: " ^ (String.concat (name_of po_causer)) ^ ", OPNAME: " ^ operation_name ^ " TYPE: " ^ pre_or_post ^ "\n")
| print_cinfo _ = print ("Print not supported now")
*)
end;

133
su4sml/src/wfcpo-gen/data_model_consistency.sml Normal file
View File

@ -0,0 +1,133 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(** Implementation of the Liskov Substitiution Principle. *)
signature DATA_MODEL_CONSISTENCY_CONSTRAINT =
sig
include BASE_CONSTRAINT
val class_model_consistency : Rep.Model -> Rep_OclTerm.OclTerm
val strong_model_consistency : Rep.Model -> Rep_OclTerm.OclTerm
end
functor Data_Model_Consistency_Constraint (SuperCon : BASE_CONSTRAINT) : BASE_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Ext_Library
open ModelImport
open Rep2String
(* ocl-parser *)
open ModelImport
open Context
(* wfcpo-gen *)
open WFCPO_Library
exception ConstraintError of string
exception BaseConstraintError of string
exception LiskovError of string
type constraint = SuperCon.constraint
fun c_allInstance_term (c:Classifier) =
let
(* create terms form right to left *)
val x = Variable("x",DummyT)
val oclIsTypeOf = OperationWithType (x,DummyT,"oclIsTypeOf",type_of c,Boolean)
val exists = Iterator("exists",[("x",DummyT)],Literal("dummy_source",DummyT),DummyT,oclIsTypeOf,Boolean,Boolean)
val allInstances = OperationCall (Literal("dummy_source",DummyT),DummyT,["oclLib","OclAny","allInstances"],[],Boolean)
val class = Literal("c",type_of c)
(* nest sources *)
val term = add_source (class,allInstances)
val term = add_source (allInstances,exists)
in
OperationCall (term,DummyT,["holOclLib","Boolean","OclLocalValid"],[],Boolean)
end
(* E t. t |= c::allInstances()->exists(x|x.oclIsTypeOf(c)) *)
fun single_model_consistency (c:Classifier) (model as (clist,alist)) =
let
val term = c_allInstance_term c
in
OperationCall (Variable("tau",DummyT),DummyT,["holOclLib","Quantor","existence"],[(term,type_of_term term)],Boolean)
end
fun class_model_consistency_help [] (model as (clist,alist)) = []
| class_model_consistency_help (h::classes) (model as (clist,alist)) =
(single_model_consistency h model)::(class_model_consistency_help classes model)
fun class_model_consistency (model as (clist,alist)) =
let
val classifiers = removeOclLibrary (clist)
in
class_model_consistency_help classifiers model
end
fun strong_model_consistency_help classes model =
let
val terms = List.map (c_allInstance_term) classes
val n_term = nest_source terms
in
OperationCall (Variable ("tau",DummyT),DummyT,["holOclLib","Quantor","existence"],[(n_term,type_of_term n_term)],Boolean)
end
fun strong_model_consistency (model as (clist,alist)) =
let
val classifiers = removeOclLibrary (clist)
in
strong_model_consistency_help classifiers model
end
fun generate_po model =
let
val po2 = class_model_consistency model
val po3 = strong_model_consistency model
in
po2@[po3]
end
end;

27
su4sml/src/wfcpo-gen/init-test-setup.sml Normal file
View File

@ -0,0 +1,27 @@
(* open structures *)
(* SU4SML *)
open OclLibrary
open ModelImport
open Rep_Core
open Ext_Library
(* WFCPO-GEN *)
open WFCPO_Library
open WFCPO_Registry
(* set debugging settings *)
val _ = Control.Print.printDepth:=10
val _ = Control.Print.printLength:=30
val zargo = "../../../examples/calendar/calendar.zargo"
val ocl="../../../examples/calendar/calendar.ocl"
(** impor model *)
val i_model = import zargo ocl []
val (clist,alist) = normalize_ext i_model
val model = ((clist@oclLib),(alist))

20
su4sml/src/wfcpo-gen/last.txt Normal file
View File

@ -0,0 +1,20 @@
SHELL:
INPUT: use "test-setup.sml"
{aend_type=Classifier ["AbstractSimpleChair02","Participant"],
init=NONE,multiplicity=[(0,~1)],
name=["AbstractSimpleChair02","association_123465",
"participants"],ordered=false,visibility=public}],
name=["AbstractSimpleChair02","association_123465"]}])
: Classifier list * association list
val x = () : unit
val y =
{description="refine from package oclLib to package oclLib",generator=fn,
name="refine"} : constraint
REFINE MODEL ...
shitCHECK SYNTAX ...
uncaught exception GetClassifierError
raised at: ocl_parser/library.sml:645.9-645.86

355
su4sml/src/wfcpo-gen/library.sml Normal file
View File

@ -0,0 +1,355 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(** This library provides different functions used in many components of the WFCPO-generator.
* This operations are used very often and therefore they are accessible over this library.
* Although they are used frequently, it does make no sense to export them to the standard ocl
* library because there just important for implementing constraints.
*)
signature WFCPO_LIBRARY =
sig
(** Get the name of a certain precondition.*)
val name_of_precondition : (string option * Rep_OclTerm.OclTerm) -> string option
(** Get the name of a certain postcondition.*)
val name_of_postcondition : (string option * Rep_OclTerm.OclTerm)-> string option
(** Get the term of a certain precondition.*)
val term_of_precondition : (string option * Rep_OclTerm.OclTerm) -> Rep_OclTerm.OclTerm
(** Get the term of a certain postcondition.*)
val term_of_postcondition : (string option * Rep_OclTerm.OclTerm) -> Rep_OclTerm.OclTerm
(** Wrap a predicate over an OclTerm.*)
val wrap_predicate : Rep_OclTerm.OclTerm -> string option -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list -> Rep_OclTerm.OclTerm
(** Conjugate a list of terms to one single term.*)
val conjugate_terms : Rep_OclTerm.OclTerm list -> Rep_OclTerm.OclTerm
(** Transform a option list to a normal list.*)
val optlist2list : 'a option list -> 'a list
(** Get a local operation by name. *)
val get_operation : string -> Rep_Core.Classifier -> Rep_Core.operation
(** Test wheter the signatures are type consistent.*)
val sig_conforms_to : (string * Rep_OclType.OclType) list -> (string * Rep_OclType.OclType) list -> Rep.Model -> bool
(** Check if the operation is a refinement of another operation.*)
val same_op : Rep_Core.operation -> Rep_Core.operation -> Rep.Model -> bool
(** *)
val class_contains_op : Rep_Core.operation -> Rep.Model -> Rep_Core.Classifier -> bool
(** Get the local operations of a classifier.*)
val local_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get the redefined/refined operations of a classifier.*)
val modified_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all the inherited (without the redefined ones) operations of a classifier.*)
val inherited_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all operations of a classifier (for redefined ones the more special is choosen).*)
val all_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all creators of a classifier.*)
val creation_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all destroying operations of a classifier.*)
val destruction_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get the class his children *)
val children_of : Rep_Core.Classifier -> Rep.Model -> Rep_OclType.Path list
(** Check inheritance tree for a given property and return first classifer fullfilling property.*)
val go_up_hierarchy : Rep_Core.Classifier -> (Rep_Core.Classifier -> bool) -> Rep.Model -> Rep_Core.Classifier
(** Get the local invariants of a classifier.*)
val local_invariants_of : Rep_Core.Classifier -> (string option * Rep_OclTerm.OclTerm) list
(** Get the inherited invarinats of a classifier.*)
val inherited_invariants_of : Rep_Core.Classifier -> Rep.Model -> (string option * Rep_OclTerm.OclTerm) list
(** Get all invariants of a classifier.*)
val all_invariants_of : Rep_Core.Classifier -> Rep.Model -> (string option * Rep_OclTerm.OclTerm) list
(** get the relative path according to the package *)
val rel_path_of : Rep_OclType.Path -> Rep_OclType.Path -> Rep_OclType.Path
(** Substitute a package name of a path. *)
val substitute_package : Rep_OclType.Path -> Rep_OclType.Path -> Rep_OclType.Path -> Rep_OclType.Path
(** Any kind of exceptions. *)
exception WFCPO_LibraryError of string
end
structure WFCPO_Library:WFCPO_LIBRARY =
struct
(* SU4SML *)
open Rep_Core
open Rep
open Rep_OclType
open Rep_OclTerm
open OclLibrary
open Rep2String
(* OclParser *)
open Ext_Library
(* WFCPO-Gen *)
open WFCPO_Naming
open Base_Constraint
exception WFCPO_LibraryError of string
fun name_of_precondition ((a:string option),(t:OclTerm)) = a
fun name_of_postcondition ((a:string option),(t:OclTerm)) = a
fun term_of_precondition ((a:string option),(t:OclTerm)) = t
fun term_of_postcondition ((a:string option),(t:OclTerm)) = t
(* FixME: adapter for info in subterm *)
(* fun holocl_adapter path (t:OclTerm) =
OperationCall (
*)
fun wrap_predicate term (NONE) args = Predicate (term,type_of_term term,[generate_name "gen_name"],args)
| wrap_predicate term (SOME(x)) args = Predicate (term,type_of_term term,[x],args)
fun conjugate_terms [] = raise WFCPO_LibraryError ("Empty list not conjugateable. \n")
| conjugate_terms [x:OclTerm] = (x)
| conjugate_terms ((h:OclTerm)::tail) =
let
val x = conjugate_terms tail
in
if (type_of_term h = Boolean)
then (OperationCall(h,type_of_term h,["oclLib","Boolean","implies"],[(x,type_of_term x)],Boolean))
else raise WFCPO_LibraryError ("type of term is not Boolean")
end
(* create normal list from a list of options type *)
fun optlist2list [] = []
| optlist2list (h::tail) =
(
case h of
NONE => optlist2list (tail)
| SOME (e) => (e::(optlist2list tail))
)
fun filter_out_none [] = []
| filter_out_none (NONE::tail) = filter_out_none tail
| filter_out_none (SOME(x)::tail) = (SOME(x)::(filter_out_none tail))
fun get_operation s classifier =
let
val x = List.find (fn a => if (name_of_op a = s) then true else false) (operations_of classifier)
in
case x of
NONE => raise WFCPO_LibraryError ("No operation found using 'get_operation'.\n")
| SOME (x) => x
end
(* check whether two given signatures match each other from the type point of view *)
fun sig_conforms_to [] [] model = true
| sig_conforms_to [] list model =
let
val result = false
in
result
end
| sig_conforms_to list [] model =
let
val result = false
in
result
end
| sig_conforms_to [(s1:string,sig_sub:OclType)] [(s2:string,sig_super:OclType)] model =
let
val result = if (conforms_to (sig_sub) (sig_super) model) then
true
else
false
in
result
end
| sig_conforms_to ((s1:string,sig_sub:OclType)::tail1) ((s2:string,sig_super:OclType)::tail2) model =
let
val result = if (s2 = s1 andalso (conforms_to (sig_sub) (sig_super) model)) then
sig_conforms_to tail1 tail2 model
else
false
in
result
end
fun same_op (sub_op:operation) (super_op:operation) (model:Model) =
if ((name_of_op sub_op = name_of_op super_op ) andalso (sig_conforms_to (arguments_of_op sub_op) (arguments_of_op super_op) model))
then true
else false
fun class_contains_op oper model classifier =
let
val ops = local_operations_of (name_of classifier) model
in
List.exists (fn a => if (#name oper) = (#name a)
andalso (sig_conforms_to (arguments_of_op oper) (arguments_of_op a) model)
then true
else false) ops
end
(* get all local operations of a classifier *)
and local_operations_of c_name model = operations_of (class_of c_name (#1 model))
fun embed_local_operation oper [] model = [oper]
| embed_local_operation lop ((oper:operation)::iops) model =
if (same_op lop oper model)
then (lop::iops)
else (oper)::(embed_local_operation lop iops model)
(* embed local operations to the inherited operations *)
fun embed_local_operations [] iops model = iops
| embed_local_operations x [] model = x
| embed_local_operations (h::tail) iops model =
let
val tmp = embed_local_operation h iops model
in
(embed_local_operations tail tmp model)
end
(* get all inherited operations of a classifier, without the local operations *)
fun inherited_operations_of c_name (model as (clist,alist)) =
let
val class = class_of c_name (#1 model)
val parents = parents_of class (#1 model)
val c_parents = List.map (fn a => class_of a (#1 model)) parents
val ops_of_par = (List.map (operations_of) c_parents)
in
List.foldr (fn (a,b) => embed_local_operations a b model) (List.last (ops_of_par)) ops_of_par
end
(* get absolutelly all operations of a classifier. In case of a functions which occurs serveral times in the inheritance tree, the must specified function is listed. *)
fun all_operations_of c_name model =
let
val lo = local_operations_of c_name model
val io = inherited_operations_of c_name model
in
embed_local_operations lo io model
end
(* get all local operations, which occurs in one of the parent classes at least each time also *)
fun modified_operations_of c_name model =
let
val io = inherited_operations_of c_name model
val lo = local_operations_of c_name model
fun op_exists (oper:operation) [] = false
| op_exists (oper:operation) ((h:operation)::tail) = if (oper=h)
then true
else op_exists oper tail
in
optlist2list (List.map (fn a => if (op_exists a io)
then NONE
else (if (List.exists (fn b => same_op a b model) io)
then SOME(a)
else NONE
)) lo)
(* List.concat (List.map (fn a => List.filter (fn b => if (same_op a b model) then false else true) io) lo ) *)
end
fun creation_operations_of c_name (model:Rep.Model) =
let
val oper = all_operations_of c_name model
val creators = List.filter (fn a => List.exists (fn b => b = "create") (#stereotypes a)) (oper)
in
creators
end
fun destruction_operations_of c_name (model:Rep.Model) =
let
val oper = all_operations_of c_name model
val creators = List.filter (fn a => List.exists (fn b => b = "destroy") (#stereotypes a)) (oper)
in
creators
end
fun go_up_hierarchy location func (model as (clist,alist)) =
let
val parent = parent_of location (#1 model)
in
if (func parent = true)
then parent
else
(if (type_of parent = OclAny)
then raise WFCPO_LibraryError ("No such property using 'go_up_hierarchy'.\n")
else go_up_hierarchy parent func model
)
end
fun children_of class (model as ([],alist)) = []
| children_of class (model as ((h::tail),alist)) =
if (parent_of h (#1 model) = class)
then (name_of h)::(children_of class ((tail,alist)))
else (children_of class ((tail,alist)))
fun has_children class (model as (clist,alist)) =
let
val ch = children_of class model
in
if (List.length (ch) = 0)
then false
else true
end
fun local_invariants_of class = invariant_of class
fun inherited_invariants_of class (model:Rep.Model as (clist,alist)) =
let
val parent = parent_of class (#1 model)
in
if (type_of parent = OclAny)
then []
else (local_invariants_of class)@(inherited_invariants_of parent model)
end
fun all_invariants_of class model =
(local_invariants_of class)@(inherited_invariants_of class model)
fun rel_path_of [] name = name
| rel_path_of [x] [y] = if (x=y) then [] else raise WFCPO_LibraryError ("rel_path_of only possible for name with same package/prefix.\n")
| rel_path_of [x] name = if (x = List.hd (name)) then (List.tl (name)) else raise WFCPO_LibraryError ("rel_path_of only possible for name with same package/prefix")
| rel_path_of package name =
if (List.hd(package) = List.hd(name)) then (rel_path_of (List.tl package) (List.tl name)) else raise WFCPO_LibraryError ("rel_path_of only possible for name with same package/prefix")
fun substitute_package [] tpackage [] = raise WFCPO_LibraryError ("Not possible to substitute package since names belongs to package itself and not a class of it.\n")
| substitute_package [] tpackage path = tpackage@path
| substitute_package x tpackage [] = raise WFCPO_LibraryError ("Not Possible to substitute Package since package longer than path.\n")
| substitute_package (hf::fpackage) (tpackage) (hp::path) =
if (hf = hp)
then substitute_package fpackage tpackage path
else (hp::path)
end;

198
su4sml/src/wfcpo-gen/liskov_constraint.sml Normal file
View File

@ -0,0 +1,198 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(** Implementation of the Liskov Substitiution Principle. *)
signature LISKOV_CONSTRAINT =
sig
include BASE_CONSTRAINT
(** sub constraint, included in liskov.*)
val weaken_precondition : Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in liskov.*)
val strengthen_postcondition : Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in liskov.*)
val conjugate_invariants : Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Liskov_Constraint (SuperCon : BASE_CONSTRAINT) : LISKOV_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Ext_Library
open ModelImport
open Rep2String
(* wfcpo-gen *)
open WFCPO_Library
open WFCPO_Naming
exception ConstraintError of string
exception BaseConstraintError of string
exception LiskovError of string
type constraint = SuperCon.constraint
fun generate_return_value typ oper sub_class super_class model =
let
val op_of_super = get_operation (name_of_op oper) super_class
val sub_name = string_of_path (name_of sub_class)
val super_name = string_of_path (name_of super_class)
val op_name = name_of_op oper
in
case typ of
(* precondition *)
(* DEFINITION (OOSC p.578):
--------------------------------
| super_pres -> sub_posts |
________________________________
*)
1 =>
let
(* preconditions of super type in one term *)
val term_super = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,["liskov","weaken precondition",super_name,op_name,(generate_opt_name "gen_pre" a)],[]))) (precondition_of_op op_of_super))
(* preconditions of sub type in one term *)
val term_sub = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,["liskov","weaken precondition",sub_name,op_name,(generate_opt_name "gen_pre" a)],[]))) (precondition_of_op oper))
in
OperationCall(term_super,Boolean,["Boolean","implies"],[(term_sub,type_of_term term_sub)],Boolean)
end
(* postcondition *)
(* DEFINITION (OOSC p.578):
--------------------------------
| sub_posts -> super_posts |
________________________________
*)
| 2 =>
let
(* postconditions of sub type in one term *)
val term_sub = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,["liskov","strengthen postcondition",sub_name,op_name,(generate_opt_name "gen_post" a)],[]))) (postcondition_of_op oper))
(* postconditions of super type in one term *)
val term_super = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,["liskov","strengthen postcondition",super_name,op_name,(generate_opt_name "gen_post" a)],[]))) (postcondition_of_op op_of_super))
in
OperationCall(term_sub,Boolean,["Boolean","implies"],[(term_super,type_of_term term_super)],Boolean)
end
| x => raise LiskovError ("Wrong Argument for generate_return_value. Only 1 (pre) and 2 (post) allowed.\n")
end
fun weaken_precondition_help [] model = []
| weaken_precondition_help (class::clist) model =
let
val mo = modified_operations_of (name_of class) model
(* (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
(* proofs obligation for classifier [(term,constraint info)] *)
val pos = List.map (fn (a,b) => generate_return_value 1 a class b model) raw_po
in
pos@(weaken_precondition_help clist model)
end
fun weaken_precondition (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
weaken_precondition_help cl model
end
fun strengthen_postcondition_help [] model = []
| strengthen_postcondition_help (class::clist) model =
let
val mo = modified_operations_of (name_of class) model
(* (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
(* proof obligations for classifier [(term,constraint info)] *)
val pos = List.map (fn (a,b) => generate_return_value 2 a class b model) raw_po
in
pos@(strengthen_postcondition_help clist model)
end
fun strengthen_postcondition (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
strengthen_postcondition_help cl model
end
fun conjugate_invariants_help [] model = []
| conjugate_invariants_help (class::clist) model =
let
(* get the invariants of all parents *)
val invariants = all_invariants_of class model
val c_name = string_of_path (name_of class)
val invs = List.map (fn (a,b) => Predicate(b,type_of_term b,["liskov","conjugate invariants",c_name,(generate_opt_name "inv" a)],[])) invariants
in
if (List.length(invs) = 0)
then (conjugate_invariants_help clist model)
else
(conjugate_terms invs)::(conjugate_invariants_help clist model)
end
fun conjugate_invariants (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
conjugate_invariants_help cl model
end
fun generate_po (model as (clist,alist)) =
let
val _ = trace zero ("generate_po: \n")
val _ = trace zero ("weaken the precondition.\n")
val x1 = weaken_precondition model
val _ = trace zero ("strengthen the postcondition.\n")
val x2 = strengthen_postcondition model
val _ = trace zero ("conjugate the invariants.\n")
val x3 = conjugate_invariants model
in
x1@x2@x3
end
end

41
su4sml/src/wfcpo-gen/logging.sml Normal file
View File

@ -0,0 +1,41 @@
(* values *)
val offset = ref 1
val quite = (log_level:= 0)
val verbose = (log_level:= 100)
fun set_log_level x =
if (x <= 0) then
(raise DebuggingError "Debugging level cannot be negative! \n")
else
log_level:=x
fun current_offset 0 = raise DebugOffsetError (" Offset 0 reached \n")
| current_offset x =
if (x = 1) then
"\t"
else
("\t" ^ (current_offset (x-1)))
fun debug_offset "inc" s x level =
let
val _ = trace high ((current_offset (!offset)) ^ s ^ " : " ^ "\n")
val _ = if (level = 0) then
log_level:= !log_level
else
log_level:= level
in
offset := !offset + 1
end
| debug_offset "dec" s 0 level = raise DebugOffsetError ("Not possible to decrease offset since it is 0.")
| debug_offset "dec" s x level =
let
val _ = trace high ((current_offset (!offset - 1)) ^ "} end " ^ s ^ "\n")
val _ = if (level = 0) then
log_level:= !log_level
else
log_level:= level
in
offset := !offset - 1
end
| debug_offset s1 s2 x level = raise DebugOffsetError ("Only 'inc' and 'dec' operations possible. \n")

59
su4sml/src/wfcpo-gen/naming.sml Normal file
View File

@ -0,0 +1,59 @@
signature WFCPO_NAMING =
sig
val get_po_number : unit -> int
val reset_po_nr : unit -> unit
val reset_count : unit -> unit
val generate_name : string -> string
val generate_opt_name : string -> string option -> string
end
structure WFCPO_Naming:WFCPO_NAMING =
struct
val po_nr = ref 0
val count = ref 0
fun get_po_number() =
let
val _ = (po_nr := ((!po_nr) + 1))
in
(!po_nr)
end
fun reset_po_nr() =
let
val _ = po_nr := 0
in
print ("po number reseted.\n")
end
fun reset_count() =
let
val _ = count := 0
in
print ("count reseted.\n")
end
fun generate_name s =
let
val _ = count := (!count + 1)
in
s ^ Int.toString (!count)
end
fun generate_opt_name s NONE =
let
val _ = count := (!count + 1)
in
generate_name s
end
| generate_opt_name s (SOME(x)) =
let
val _ = count := (!count + 1)
in
x
end
end;

130
su4sml/src/wfcpo-gen/operational_consistency.sml Normal file
View File

@ -0,0 +1,130 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(** Implementation of the wellformed constraint for a constructor *)
signature OPERATIONAL_CONSTRAINT =
sig
include BASE_CONSTRAINT
(** sub constraint, included in operational consistency.*)
val generate_class_constraints : Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in operational consistency.*)
val generate_operation_constraints : Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in operational consistency.*)
val generate_attribute_constraints : Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Operational_Constraint (SuperCon : BASE_CONSTRAINT) : OPERATIONAL_CONSTRAINT =
struct
(* SU4SML *)
open Rep_Core
open Rep
open Rep_OclTerm
open Rep_OclType
(* OclParser *)
open Ext_Library
open ModelImport
(* WFCPO *)
open WFCPO_Naming
open WFCPO_Library
exception ConstraintError of string
exception BaseConstraintError of string
exception ConstructorError of string
type constraint = Constraint.constraint
(*
fun generate_class_constraints_single classe (model as (clist,alist)) =
(* [Variable("s",DummyT)] *)
let
val creators = creation_operations_of
val x = List.map (fn a =>
in
end
*)
fun generate_operation_constraints_help classes (model as (clist,alist)) = [Variable("s",DummyT)]
fun generate_attribute_constraints_help classes (model as (clist,alist)) = [Variable("s",DummyT)]
(**
tink about which classes to filter.
Maybe the classes from the SecureUML metamodel
must be deletet to.
**)
fun generate_class_constraints (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
in
generate_class_constraints_help classes model
end
fun generate_operation_constraints (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
in
generate_operation_constraints_help classes model
end
fun generate_attribute_constraints (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
in
generate_attribute_constraints_help classes model
end
fun generate_po (model as (clist,alist)) = (* [Variable("s",DummyT)] *)
let
(* val po1 = generate_class_constraints model
val po2 = generate_operation_constraints model
val po3 = generate_attribute_constraints model
*) in
[] (* po1@po2@po3 *)
end
end;

30
su4sml/src/wfcpo-gen/plugin_constraint.sml Normal file
View File

@ -0,0 +1,30 @@
signature PLUGIN_CONSTRAINT =
sig
include CONSTRAINT
val getConstraint : Constraint.constraint
val info : string
val generate_po : Rep.Model -> Rep_OclTerm.OclTerm list
exception Plugin_Constraint_Error of string
end
structure Plugin_Constraint : PLUGIN_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep
open Rep_OclTerm
(* wfcpo-gen *)
open Constraint
type constraint = Constraint.constraint
exception ConstraintError of string
exception Plugin_Constraint_Error of string
fun generate_po (model:Rep.Model) = [Predicate (Literal("true",Boolean),Boolean,["DUMMY_PREDICATE"],[])]
val getConstraint = {name="plugin_constraint",description="A plugin_constraint cannot be instantiated itself. Use a corresponding plugin.\n",generator=generate_po}:constraint
val info = "This is just the structure. For creating a new plugin constraint, write a functor implementing the PLUGIN_CONSTRAINT signature. The a new constraint can be registered in the WFCPO_Registry by add the structure NEW_FUNCTOR(Plugin) and calling the value newConstraint."
end;

250
su4sml/src/wfcpo-gen/refine_constraint.sml Normal file
View File

@ -0,0 +1,250 @@
signature REFINE_CONSTRAINT =
sig
include PLUGIN_CONSTRAINT
val setPackages : Rep_OclType.Path -> Rep_OclType.Path -> unit
val refine_model : Rep_OclType.Path -> Rep_OclType.Path -> Rep.Model -> (Rep_OclTerm.OclTerm * string) list
val FromPack : Rep_OclType.Path ref
val ToPack : Rep_OclType.Path ref
exception RefineError of string
exception ClassGroupError of Rep_Core.Classifier list * string
exception OpGroupError of Rep_Core.operation list * string
exception WFCPO_SyntaxError_ClassConsistency of (Rep_OclType.Path * Rep_Core.Classifier list)
exception WFCPO_SyntaxError_OpConsistency of (Rep_Core.Classifier * Rep_Core.operation list)
exception WFCPO_SyntaxError_TypeConsistency of (Rep_Core.Classifier * Rep_Core.Classifier * Rep_Core.operation * Rep_Core.operation)
end
functor Refine_Constraint(SuperCon : PLUGIN_CONSTRAINT)(* : REFINE_CONSTRAINT *) =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
(* ocl-parser *)
open Ext_Library
(* wfcpo-gen *)
open Base_Constraint
open WFCPO_Library
exception WFCPO_SyntaxError_ClassConsistency of (Path * Classifier list)
exception WFCPO_SyntaxError_OpConsistency of (Classifier * operation list)
exception WFCPO_SyntaxError_TypeConsistency of (Classifier * Classifier * operation * operation)
exception Plugin_Constraint_Error of string
exception ClassGroupError of Rep_Core.Classifier list * string
exception OpGroupError of Rep_Core.operation list * string
exception RefineError of string
type constraint = SuperCon.constraint
val FromPack = ref ["AbstractSimpleChair01"]
val ToPack = ref ["ConcreteSimpleChair01"]
fun setPackages (p1) (p2) =
let
val x = FromPack := p1
val y = ToPack := p2
in
print ("Packages set from " ^ (string_of_path p1) ^ " to " ^ (string_of_path p2) ^ "\n")
end
fun rm x [] = []
| rm x [b] = if (x = b) then [] else [b]
| rm x (h::tail) = if (x = h) then (rm x tail) else (h::(rm x tail))
fun group_cl [] [] = []
| group_cl [] toC = []
| group_cl FromC [] = raise ClassGroupError (FromC,("Some classes of the abstract package are public where in the concrete not.\n"))
| group_cl (h1::t1) list =
let
val _ = trace zero ("Class: " ^ string_of_path (name_of h1) ^ "\n")
val x = List.filter (fn a => ((List.last (name_of a)) = (List.last (name_of h1)))) list
(* val _ = trace high ("fromClass = " ^ (string_of_path (name_of h1)) ^ ", toClass = " ^ (string_of_path (name_of (hd(x)))) ^ "\n") *)
in
if (List.length(x) = 0)
then raise ClassGroupError ([h1],("Some classes of the abstract package are public where in the concrete not.\n"))
else (h1,hd(x))::(group_cl t1 (rm (hd(x)) list))
end
fun group_op [] [] = []
| group_op fromOps [] = raise OpGroupError (fromOps,("Some operations of the abstract class are public where int the concrete not.\n"))
| group_op [] toOps = []
| group_op ((h1:operation)::t1) list =
let
val x = hd(List.filter (fn a => ((name_of_op a) = (name_of_op h1))) list)
in
(h1,x)::(group_op t1 (rm x list))
end
(* RETURN: (Classifier * Classifer) list *)
fun map_public_classes fromPath toPath (model as (clist,alist)) =
let
val _ = trace zero ("MAP_PUBLIC_CLASSES ...\n")
val abs_c = List.filter (is_visible_cl) (List.filter (fn a => if (package_of a = fromPath) then true else false) (clist))
val _ = printList abs_c
val _ = trace zero ("map_public_classes 2 \n")
val _ = trace zero ("Package " ^ string_of_path (fromPath) ^ " contains " ^ Int.toString (List.length(abs_c)) ^ " classes.\n")
val conc_c = List.filter (is_visible_cl) (List.filter (fn a => if (package_of a = toPath) then true else false) (clist))
val _ = printList conc_c
val _ = trace zero ("Package " ^ string_of_path (toPath) ^ " contains " ^ Int.toString (List.length(conc_c)) ^ " classes.\n")
val _ = trace zero ("map_public_classes 3 \n")
in
group_cl abs_c conc_c
handle ClassGroupError (clist,s) =>
let
val _ = trace exce ("\n\n#####################################################################\n")
val _ = trace exce ("#####################################################################\n\n")
val _ = trace exce ("SYNTAX ERROR: Class consistency \n\n")
val _ = trace exce ("The following public classes are not included in the refined class:\n\n")
val _ = trace exce (String.concat (List.map (fn a => (" * " ^ (string_of_path (name_of a)) ^ "\n")) clist))
in
raise RefineError ("Please adjust model...\n")
end
end
fun map_public_ops [] = [[]]
| map_public_ops ((f,t)::tail) =
let
val _ = trace zero ("MAP_PUBLIC_OPS ... \n")
val f_ops = List.filter (is_visible_op) (operations_of f)
val t_ops = List.filter (is_visible_op) (operations_of t)
val _ = trace zero ("Number of operations of f_class(" ^ (string_of_path (name_of f)) ^ ") = " ^ Int.toString (List.length(f_ops)) ^ "\n")
val _ = trace zero ("Number of operations of t_class(" ^ (string_of_path (name_of t)) ^ ") = " ^ Int.toString (List.length(t_ops)) ^ "\n")
in
[(List.map (fn (a,b) => (f,t,a,b)) (group_op f_ops t_ops
handle OpGroupError (oplist,s) =>
let
val _ = trace exce ("\n\n#####################################################################\n")
val _ = trace exce ("#####################################################################\n\n")
val _ = trace exce ("SYNTAX ERROR: Operation consistency \n\n")
val _ = trace exce ("FromClass = " ^ (string_of_path (name_of f)) ^ "\n")
val _ = trace exce ("ToClass = " ^ (string_of_path (name_of t)) ^ "\n")
val _ = trace exce ("The following public operations are not included in the refined classes:\n\n")
val _ = trace exce (String.concat (List.map (fn a => (" * " ^ (operation2string a) ^ "\n")) oplist))
in
raise RefineError ("Please adjust model...\n")
end
))]
@(map_public_ops tail)
end
fun map_types [] fP tP model = []
| map_types ((h1:Classifier,h2:Classifier,h3:operation,h4:operation)::tail) fP tP model =
let
val _ = trace zero ("MAP_TYPES ... \n")
val _ = trace zero ("map_types: f_cl = " ^ string_of_path (name_of h1) ^ "\n")
val _ = trace zero ("map_types: f_cl = " ^ string_of_path (name_of h2) ^ "\n")
val _ = trace zero ("map_types: f_op = " ^ name_of_op h3 ^ "\n")
val _ = trace zero ("map_types: t_op = " ^ name_of_op h4 ^ "\n")
(* classifier of return type *)
val ret_fC = class_of_type (#result (h3)) model
val _ = trace zero ("map_types 2 \n")
(* name of classifier of return type *)
val ret_namefC = name_of ret_fC
val _ = trace zero ("map_types_3: " ^ string_of_path (ret_namefC) ^ "\n")
val _ = trace zero ("map_types_4: " ^ string_of_path fP ^ "\n")
(* relative path of return type *)
val new_path = substitute_package fP tP ret_namefC
val _ = trace zero ("map_types_5: name of return type: " ^ string_of_path (ret_namefC) ^ "\n")
val c1 = class_of (new_path) (#1 model)
handle _ =>
let
val _ = trace exce ("\n\n#####################################################################\n")
val _ = trace exce ("#####################################################################\n\n")
val _ = trace exce ("SYNTAX ERROR: Map types \n\n")
val _ = trace exce ("The return type of the operation " ^ (operation2string h3) ^ " is inconsistent.\n")
val _ = trace exce ("The refining package has no corresponding class.\n")
val _ = trace exce ("Existing FromClass = " ^ (string_of_path (name_of h1)) ^ "\n")
val _ = trace exce ("Inexisting ToClass = " ^ (string_of_path (name_of h2)) ^ "\n")
in
raise RefineError ("Please adjust model...\n")
end
(* name of the arguments *)
val _ = trace zero ("map_types_6: " ^ string_of_path (name_of c1) ^ "\n")
val arg_class_name1 = List.map (fn (a,b) => (name_of (class_of_type b model))) (arguments_of_op (h3))
val _ = trace zero ("map_types_7: \n")
val c2 = List.map (fn a =>
let
val rel_path = substitute_package fP tP a
in
class_of (rel_path) (#1 model)
handle _ =>
let
val _ = trace exce ("\n\n#####################################################################\n")
val _ = trace exce ("#####################################################################\n\n")
val _ = trace exce ("SYNTAX ERROR: Map types \n\n")
val _ = trace exce ("One of the arguments type of the operation " ^ (operation2string h3) ^ " is inconsistent.\n")
val _ = trace exce ("The refining package has no corresponding class.\n")
val _ = trace exce ("Existing FromClass = " ^ (string_of_path (name_of h1)) ^ "\n")
val _ = trace exce ("Inexisting ToClass = " ^ (string_of_path (name_of h2)) ^ "\n")
in
raise RefineError ("Please adjust model...\n")
end
end
) arg_class_name1
val _ = trace zero ("map_types_8: \n")
in
(true)::(map_types tail fP tP model)
end
fun check_syntax fromPath toPath (model:Rep.Model as (clist,alist)) =
let
val _ = trace zero ("CHECK SYNTAX ... \n")
(* check public classes of the two packages *)
val x = map_public_classes fromPath toPath model
val _ = trace zero ("check syntax 2 \n")
(* check public methods of the public classes *)
val y = List.concat (map_public_ops x)
val _ = trace zero ("check syntax 3 \n")
(* check types of the public operations of public classes *)
val z = map_types y fromPath toPath model
val _ = trace zero ("check syntax 4 \n")
in
List.all (fn a => a) z
handle _ => raise RefineError ("Something undetermined happened. Shit!.\n")
end
(*
fun refine_semantics [] (model:Rep.Model) = []
| refine_semantics ((fromC,toC)::tail) (model as (clist,alist)) =
*)
(*
fun rule_1
fun rule_2
fun rule_3
*)
fun refine_model fromPath toPath (model:Rep.Model) =
let
val _ = trace zero ("REFINE MODEL ...\n")
val _ = trace zero ("shit")
val x = check_syntax fromPath toPath model
val _ = trace zero ("output of syntax check : " ^ Bool.toString x ^ "\n")
(* val po1 = rule_1 fromPath toPath model
val po2 = rule_2 fromPath toPath model
val po3 = rule_3 fromPath toPath model *)
in
(* po1@po2@po3 *)
[(Literal("true",Boolean))]
end
val getConstraint =
{ name = "refine",
description = ("refine from package " ^ (string_of_path (!FromPack)) ^ " to package " ^ (string_of_path (!ToPack))),
generator = refine_model (!FromPack) (!ToPack) }:Constraint.constraint
val info = "\n\nCREATION OF A NEW REFINE CONSTRAINT: \n\ni.) call: Refine.setPackages pack1 pack2\n where pack1 is the package to be replaced and pack2 the one who is replacing.\nii.) call: getConstraint , for getting Constraint with the pack1 and pack2.\n\n\n"
end

154
su4sml/src/wfcpo-gen/registry.sml Normal file
View File

@ -0,0 +1,154 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
(**
* This registry a provides a list of constraints which can be applied to a given UML/OCL model.
* All the implemented constraints are accessible form this component.
* For the ease of use a default constraint list is provided by the signature. This constraint list
* can be modified to add or remove constraints form the default constraint list. New constraints
* can be generated by writing a new file implementing the WFCPO_CONSTRAINT signature.
*)
signature WFCPO_REGISTRY =
sig
val analyze_model : string -> string -> Constraint.constraint list -> Rep_OclTerm.OclTerm list
val supported_constraints : (Constraint.constraint list)
val getConstraint : string -> Constraint.constraint list -> Constraint.constraint
(** Any kind of exceptions *)
exception RegistryError of string
end
structure WFCPO_Registry (* : WFCPO_REGISTRY *) =
struct
(* SU4SML *)
open Rep_Core
open Rep
open Rep_OclTerm
open Rep_OclType
open OclLibrary
(* OclParser *)
open Ext_Library
open ModelImport
(* WFCPO *)
open WFCPO_Library
open WFCPO_Naming
(*** IMPORTED STRUCTURES ***)
(** BASE CONSTRAINTS *)
structure Con = Constraint
structure Base = Base_Constraint
structure Plugin = Plugin_Constraint
(** STATIC CONSTRAINTS *)
(* Liskov *)
structure Liskov = Liskov_Constraint(Base)
(* Data model consistency *)
structure Data = Data_Model_Consistency_Constraint(Base)
(* Constructor consistency *)
structure Constructor = Constructor_Constraint(Base)
(* Operational consistency *)
structure Operational = Operational_Constraint(Base)
(** PLUGIN CONSTRAINTS *)
(* Refinement *)
structure Refine = Refine_Constraint(Plugin)
(*** TYPES ***)
type constraint = Constraint.constraint
(*** EXCEPTIONS ***)
exception RegistryError of string
exception WFCPO_SyntaxError_ClassConsistency = Refine.WFCPO_SyntaxError_ClassConsistency
exception WFCPO_SyntaxError_OpConsistency = Refine.WFCPO_SyntaxError_OpConsistency
exception WFCPO_SyntaxError_TypeConsistency = Refine.WFCPO_SyntaxError_TypeConsistency
val supported_constraints = [
(* Liskov Substitution Principle *)
{ name = "liskov",
description = "liskov substitution principle",
generator = Liskov.generate_po},
{ name = "data model consistency",
description = "data model consistency using single model consistency, class model consistency and strong model consistency.",
generator = Data.generate_po},
{ name = "constructor consistency",
description = "constructor consistency. sub1: post -> inv",
generator = Constructor.generate_po}]
fun getConstraint s [] = raise RegistryError ("Constraint not found.\n")
| getConstraint s ((h:constraint)::tail) =
if (#name h) = s
then h
else (getConstraint s tail)
fun name_po s [] = []
| name_po s (h::tail) =
(Predicate (h,type_of_term h,[(s ^ Int.toString (get_po_number()))],[]))::(name_po s tail)
fun analyze_model_m [] model = []
| analyze_model_m (({name=n,generator=gen,...}:constraint)::tail) model =
let
val _ = trace zero ("analyzse a " ^ n ^ " constraint.\n")
in
(name_po n (gen model))@(analyze_model_m tail model)
end
fun analyze_model xmi_file ocl_file [] = raise RegistryError ("No constraints listed.\n")
| analyze_model xmi_file ocl_file con_list =
let
val _ = trace zero ("\n\n#####################################\nSTART: WFCPO \n")
val _ = trace zero ("#####################################\n")
val i_model = import xmi_file ocl_file []
val n_model = normalize_ext i_model
val model = ((#1 n_model@oclLib),(#2 n_model))
val _ = trace zero ("[*] model analyzed \n")
(* init number generator *)
val _ = reset_po_nr()
in
analyze_model_m con_list model
end
end;

87
su4sml/src/wfcpo-gen/syntax_error_db.sml Normal file
View File

@ -0,0 +1,87 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
signature WFCPO_SYNTAX_ERROR_DB =
sig
datatype SyntaxError =
SEType of
{ fromClass : Rep_Core.Classifier,
toClass : Rep_Core.Classifier,
fromOp : Rep_Core.operation,
toOp : Rep_Core.operation }
| SEOp of
{ fromClass : Rep_Core.Classifier,
ops : Rep_Core.operation list }
| SEClass of
{ package : Rep_OclType.Path,
classes : Rep_Core.Classifier list}
val SE_db : ((SyntaxError option) list) ref
val add_syntax_error : SyntaxError -> unit
end;
structure WFCPO_Syntax_Error_DB:WFCPO_SYNTAX_ERROR_DB =
struct
open Rep_Core
open Rep_OclType
datatype SyntaxError =
SEType of
{ fromClass : Classifier,
toClass : Classifier,
fromOp : operation,
toOp : operation }
| SEOp of
{ fromClass : Classifier,
ops : operation list }
| SEClass of
{ package : Path,
classes : Classifier list }
val SE_db:SyntaxError option list ref = ref [NONE]
fun add_syntax_error (s:SyntaxError) =
let
val x = (SOME(s)::(!SE_db))
in
SE_db := x
end
end;

95
su4sml/src/wfcpo-gen/test-setup.sml Normal file
View File

@ -0,0 +1,95 @@
(**************************************************************)
(****************** OPEN STRUCTURES ***************************)
(**************************************************************)
(* SU4SML *)
open OclLibrary
open ModelImport
open Rep_Core
open Ext_Library
(* WFCPO-GEN *)
open WFCPO_Library
open WFCPO_Naming
open WFCPO_Registry
(* set debugging settings *)
val _ = Control.Print.printDepth:=20
val _ = Control.Print.printLength:=80
val _ = log_level:=2
(**************************************************************)
(************** IMPORT PLUGING STRUCTURES *********************)
(**************************************************************)
structure Plugin = Plugin_Constraint
structure Refine = Refine_Constraint(Plugin)
(**************************************************************)
(***** USE REGISTRY FOR GENERATING PROOF OBLIGATIONS *********)
(**************************************************************)
(* There are several ways of getting a constraint:
*
* i.) using the default constraints:
*
* 1.) using all the default constraints:
* val supported_constraints
* 2.) using individual default Constraints:
* fun getConstraint con_name
* (e.g. getConstraint "liskov")
*
* ii.) using the plugin constraints :
*
* ATTENTION: Configure the constraint according
* to the info provided!
*
* iii.) using sub constraints of the default constraints:
*
* The corresponding interface of the constraints
* tells you which sub constraints can be exported.
* All the operations with the type:
*
* Rep.Model -> OclTerm list
*
* Then you can create manually new sub constraints.
* E.g. weaken precondition:
* structure Liskov = Liskov_Constraint(Base_Constraint)
* val newC =
* {
* name="liskov",
* description="liskov substitution principle",
* generator=Liskov.weaken_precondition
* }
*
*
***************************************************************)
(** get the static constraints *)
val l = getConstraint "liskov" supported_constraints
val dmc = getConstraint "data model consistency" supported_constraints
(** configure the plugin constraints *)
val x = Refine.setPackages ["AbstractSimpleChair01"] ["ConcreteSimpleChari01"];
(** get the plugin constraints *)
val r = Refine.getConstraint
(** build constraint list *)
val my_con_list = [l,dmc,r]
(** execute wfcpo-generator *)
(** REMARK:
* in the end the normal call will be:
*
* analyze_model "stack.zargo" "stack.ocl" my_con_list
*
* so the reset_po_nr() is not necessary any more!
**)
val _ = reset_po_nr()
val z = analyze_model_m my_con_list model

19
su4sml/src/wfcpo-gen/values.sml Normal file
View File

@ -0,0 +1,19 @@
open Rep_Core
open Rep
open ModelImport
open Rep_OclType
open Ext_Library
open WFCPO_Library
open WFCPO_Registry
open Rep2String
(* impor model *)
val i_model = import "../../../examples/stack_manu/stack.zargo" "../../../examples/stack_manu/stack.ocl" []
val n_model = normalize_ext i_model
val model = ((#1 n_model@oclLib),(#2 n_model))
(* extract classifier *)

66
su4sml/src/wfcpo-gen/wfcpo.cm Normal file
View File

@ -0,0 +1,66 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* parser.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above
* copyright notice, this list of conditions and the following
* disclaimer in the documentation and/or other materials provided
* with the distribution.
*
* * Neither the name of the copyright holders nor the names of its
* contributors may be used to endorse or promote products derived
* from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)
(* $Id: parser.cm 6700 2007-07-23 05:26:05Z brucker $ *)
Group is
../su4sml_core.cm
../su4sml.cm
../ocl_parser/parser.cm
#if(defined(SMLNJ_VERSION) && (SMLNJ_MINOR_VERSION < 60))
$/basis.cm
$/ml-yacc-lib.cm
#endif
#if(defined(SMLNJ_VERSION) && (SMLNJ_MINOR_VERSION >= 60))
$smlnj/basis/basis.cm
$smlnj/ml-yacc/ml-yacc-lib.cm
#endif
"naming.sml"
"constraint.sml"
"base_constraint.sml"
"plugin_constraint.sml"
"library.sml"
"liskov_constraint.sml"
"data_model_consistency.sml"
"constructor_consistency.sml"
(* "operational_consistency.sml" *)
"refine_constraint.sml"
"registry.sml"

26
su4sml/src/wfcpo-gen/wfcpo_init.sml Normal file
View File

@ -0,0 +1,26 @@
(* fun import xmifile oclfile ExcludePackages : string -> string -> string list -> Rep_Core.transform_model *)
open Rep_Core
open ModelImport
open Rep_Transform
open OclLibrary
open Ext_Library
(* adjust print depth *)
val _ = Control.Print.printDepth:=100
val _ = Control.Print.printLength:=100
val _ = log_level:=25
(*
use "constraints.sml"
open WFCPO_Constraints;
use "values.sml"
*)
(*
val model = transformClassifiers_ext n_model
*)