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

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

This commit is contained in:
Manuel Krucker 2008-03-31 11:24:14 +00:00
parent 75c3447bed
commit 83ece1d877
5 changed files with 162 additions and 125 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

211
su4sml/src/rep_ocl.sml
View File

@ -49,6 +49,7 @@ sig
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType
| Tuple of (OclType * OclType)
| Classifier of Path | OclVoid | DummyT | TemplateParameter of string
val short_name_of_OclType: OclType -> string
@ -70,50 +71,65 @@ include REP_OCL_TYPE
datatype OclTerm =
Literal of string * OclType (* Literal with type *)
| CollectionLiteral of CollectionPart list
* OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| QualifiedAssociationEndCall of OclTerm * OclType (* source *)
* (OclTerm * OclType) list (* qualies*)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AssociationEndCall of OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| 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 *)
* OclTerm * OclType (* in *)
| Iterate of (string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm * OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
| TupleLiteral of
OclTerm * OclType (* first of typle *)
* OclTerm * OclType (* second of typle *)
| CollectionLiteral of CollectionPart list
* OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| QualifiedAssociationEndCall of
OclTerm * OclType (* source *)
* (OclTerm * OclType) list (* qualies*)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AssociationEndCall of
OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of
OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of
OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| 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 *)
* OclTerm * OclType (* in *)
| Iterate of
(string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of
string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm
* OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
end
@ -129,6 +145,7 @@ datatype OclType = Integer | Real | String | Boolean | OclAny
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType | OclVoid | DummyT
| Tuple of (OclType * OclType)
| Classifier of Path
| TemplateParameter of string
@ -207,51 +224,69 @@ struct
open Rep_OclType
datatype OclTerm =
Literal of string * OclType (* Literal with type *)
| CollectionLiteral of CollectionPart list * OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| QualifiedAssociationEndCall of OclTerm * OclType (* source *)
* (OclTerm * OclType) list (* qualies*)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AssociationEndCall of OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| 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 *)
* OclTerm * OclType (* in *)
| Iterate of (string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm * OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
Literal of string * OclType (* Literal with type *)
| TupleLiteral of
OclTerm * OclType (* first of typle *)
* OclTerm * OclType (* second of typle *)
| CollectionLiteral of CollectionPart list
* OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| QualifiedAssociationEndCall of
OclTerm * OclType (* source *)
* (OclTerm * OclType) list (* qualies*)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AssociationEndCall of
OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of
OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of
OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| 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 *)
* OclTerm * OclType (* in *)
| Iterate of
(string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of
string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm
* OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
end

4
su4sml/src/wfcpo-gen/data.sml
View File

@ -30,8 +30,8 @@ val rfm_syn = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "rfm_syn"
val tax = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "tax"
val rfm_SC = WFCPOG_Registry.rename_wfpo "rfm_SC" (WFCPOG_Registry.RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair01"],["ConcreteSimpleChair01"])]}) rfm_syn)
val md0 = WFCPOG_Registry.rename_wfpo "md0" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=0}) tax)
val md1 = WFCPOG_Registry.rename_wfpo "md1" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=1}) tax)
val md2 = WFCPOG_Registry.rename_wfpo "md2" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=2}) tax)
@ -42,6 +42,6 @@ val md6 = WFCPOG_Registry.rename_wfpo "md6" (WFCPOG_Registry.TAX_Data.put ({key=
val md7 = WFCPOG_Registry.rename_wfpo "md7" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=7}) tax)
val md8 = WFCPOG_Registry.rename_wfpo "md8" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=8}) tax)
val wfs = [inf,vis,md0,md1,md2,md3,md4,md5,md6,md7,md8,rfm_SC]
val pos = [lsk,cm,sm,om,cmd,quy]

49
su4sml/src/wfcpo-gen/refine_constraint.sml
View File

@ -103,11 +103,10 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) =
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))
val s1 = ("SYNTAX ERROR: Class consistency \n\n")
val s2 = ("The following public classes are not included in the refined class:\n\n")
val s3 = (String.concat (List.map (fn a => (" * " ^ (string_of_path (name_of a)) ^ "\n")) clist))
val _ = trace exce (s1^s2^s3)
in
raise WFCPOG_RefineError ("Please adjust model...\n")
end
@ -116,31 +115,33 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) =
fun map_public_ops [] = [[]]
| map_public_ops ((f,t)::tail) =
let
val _ = trace zero ("MAP_PUBLIC_OPS ... \n")
val _ = trace function_calls ("Refine_Constraint.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")
val res =
[(List.map (fn (a,b) => (f,t,a,b)) (group_op f_ops t_ops
handle OpGroupError (oplist,s) =>
let
val s1 = ("SYNTAX ERROR: Operation consistency \n\n")
val s2 = ("FromClass = " ^ (string_of_path (name_of f)) ^ "\n")
val s3 = ("ToClass = " ^ (string_of_path (name_of t)) ^ "\n")
val s4 = ("The following public operations are not included in the refined classes:\n\n")
val s5 = (String.concat (List.map (fn a => (" * " ^ (operation2string a) ^ "\n")) oplist))
val _ = trace exce (s1^s2^s3^s4^s5)
in
raise WFCPOG_RefineError ("Please adjust model...\n")
end
))]
@(map_public_ops tail)
val _ = trace function_ends ("Refine_Constraint.map_public_op\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 WFCPOG_RefineError ("Please adjust model...\n")
end
))]
@(map_public_ops tail)
res
end
fun map_types [] fP tP model = []
| map_types ((h1:Classifier,h2:Classifier,h3:operation,h4:operation)::tail) fP tP model =
let

7
su4sml/src/wfcpo-gen/test-suite.sml
View File

@ -1,7 +1,7 @@
signature WFCPOG_TESTSUITE =
sig
val runTests : WFCPOG.wfpo list -> WFCPOG.wfpo list -> unit
val runTest : WFCPOG.wfpo list -> WFCPOG.wfpo list -> unit
val runTest : string -> WFCPOG.wfpo list -> WFCPOG.wfpo list -> unit
val set_printDepth : int -> unit
val set_printLength : int -> unit
end
@ -158,9 +158,10 @@ fun print_tc (tc:testcase)=
start_tc^name
end
fun runTest wfs pos =
fun runTest name wfs pos =
let
val string = (print_tc testcase)^(test testcase wfs pos)
val tc = valOf (List.find (fn a => name = (#name a)) testcases)
val string = (print_tc tc)^(test tc wfs pos)
in
if (String.isSubstring "[Error]" string)
then print(string^"\n\n !!!!!!!!!! WFCPOG still contains bugs !!!!!!!!!!!!!\n\n\n")

16
su4sml/src/wfcpo-gen/wfcpog_registry.sml
View File

@ -41,11 +41,11 @@
signature WFCPOG_REGISTRY =
sig
(* WHY?:
structure LSK_Data : WFPO_DATA
structure TAX_Data : WFPO_DATA
structure RFM_Data : WFPO_DATA
*)
val supported : WFCPOG.wfpo list
val wfpos : WFCPOG.wfpo list ref
@ -69,9 +69,9 @@ struct
exception WFCPOG_RegistryError of string
structure LSK_Data = Liskov_Constraint.LSK_Data
(*structure TAX_Data = Taxonomy_Constraint.TAX_Data
structure TAX_Data = Taxonomy_Constraint.TAX_Data
structure RFM_Data = Refine_Constraint.RFM_Data
*)
open Rep_Logger
open WFCPOG
@ -85,7 +85,7 @@ fun add_wfpo wfpo = ((wfpos := [wfpo]@(!wfpos));())
fun del_wfpo wfpo_id = ((wfpos := List.filter (fn w => not ((WFCPOG.id_of w) = (wfpo_id)) )
(!wfpos));())
fun get_wfpo [] x = raise WFCPOG_RegistryError ("No such ID found in given list!\n")
fun get_wfpo [] x = raise WFCPOG_RegistryError ("No ID = " ^ x ^ " found in given list!\n")
| get_wfpo (h::tail) x =
if (id_of h = x)
then h
@ -257,9 +257,9 @@ val supported = [
recommends = [],
apply = WFCPOG.WFC(Visibility_Constraint.are_conditions_visible),
data = Datatab.empty
}(*,
},
WFCPOG.WFPO{
identifier = "tax", (* identifier *)
identifier = "tax",
name = "Max Depth",
description = "Max Depth",
recommended = true,
@ -277,7 +277,7 @@ val supported = [
recommends = [],
apply = WFCPOG.WFC(Refine_Constraint.check_syntax),
data = Datatab.empty
}*)(*,
}(*,
WFCPOG.WFPO {
identifier = "ref_po",
name = "OO Refinement",