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

Merged su4sml-wfcpog 7219:7374 back to trunk 

git-svn-id: https://projects.brucker.ch/su4sml/svn/su4sml/trunk@7375 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2008-03-14 14:03:23 +00:00
parent 52ee5305d6
commit 85c95e432d
29 changed files with 2125 additions and 658 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -48,6 +48,7 @@ sig
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.transform_model -> Rep_Core.Classifier
val path_to_type : Rep_OclType.Path -> Rep_OclType.OclType
val get_classifier : Rep_OclTerm.OclTerm -> Rep_Core.transform_model -> Rep_Core.Classifier
val package_of_template_parameter : Rep_OclType.OclType -> string list
@ -450,6 +451,7 @@ fun string_to_type ["Integer"] = Integer
| string_to_type ["DummyT"] = DummyT
| string_to_type ["String"] = String
| string_to_type ["OclVoid"] = OclVoid
| string_to_type (("oclLib")::tail) = string_to_type tail
| string_to_type [set] =
if (List.exists (fn a => if (a = (#"(")) then true else false) (String.explode set)) then
(* set *)
@ -543,6 +545,7 @@ fun substitute_operations typ [] = []
val _ = trace low ("\n\nsubstitute operation : " ^ (#name oper) ^ " ... \n")
val args = substitute_args typ (#arguments oper)
val res = substitute_typ typ (#result oper)
val _ = trace 100 ("check\n")
in
({
name = #name oper,
@ -572,7 +575,9 @@ fun substitute_classifier typ classifier =
val _ = trace low ("substitute classifier: parameter type: " ^ string_of_OclType typ ^ " template type: " ^ string_of_OclType (type_of classifier) ^ "\n")
val styp = substitute_typ typ (type_of classifier)
val ops = substitute_operations typ (operations_of classifier)
val _ = trace 100 ("substitute parent.\n")
val sparent = substitute_parent typ
val _ = trace 100 ("end substitute parent.\n")
in
(Class
{
@ -605,7 +610,7 @@ fun substitute_classifier typ classifier =
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")) c
val _ = map (fn a => trace development (string_of_OclType (type_of a) ^ "manu type: \n")) c
fun class_of_t typ m =
hd (List.filter (fn a => if ((type_of a) = typ) then true else false) m)
in
@ -675,6 +680,19 @@ and templ_of temp_typ para_typ [] = raise TemplateInstantiationError ("Error dur
and class_of_type typ (model:Rep_Core.transform_model) =
get_classifier (Variable ("x",typ)) model
fun path_to_type (name:Path) =
case name of
["oclLib","OclAny"] => OclAny
| ["oclLib","Integer"] => Integer
| ["oclLib","Boolean"] => Boolean
| ["oclLib","Real"] => Real
| ["oclLib","String"] => String
| ["oclLib","OclVoid"] => OclVoid
| (("oclLib")::tail) => string_to_type tail
| x => Classifier(x)
(* RETURN: Boolean *)
fun conforms_to_up _ OclAny (_:Rep_Core.transform_model) = true
| conforms_to_up (Set(T1)) (Collection(T2)) model =

12
su4sml/src/rep_core.sml
View File

@ -235,6 +235,7 @@ val body_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val result_of_op : operation -> Rep_OclType.OclType
val postcondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val name_of_op : operation -> string
val name_of_ae : associationend -> Rep_OclType.Path
val mangled_name_of_op : operation -> string
val class_of : Rep_OclType.Path -> Classifier list -> Classifier
@ -454,7 +455,7 @@ fun consistency_constraint cls_name (aend,revAend) =
of [(0,1)] => false
| [(1,1)] => false
| M => true
fun mkCollection a = if (#ordered a)
fun mkCollection (a:associationend) = if (#ordered a)
then (Sequence (#aend_type a))
else (Set (#aend_type a))
@ -1251,7 +1252,9 @@ fun postcondition_of_op ({postcondition, ...}:operation) =
| il => il)
fun name_of_op ({name,...}:operation) = name
fun name_of_ae ({name,...}:associationend) = name
fun mangled_name_of_op ({name,arguments,result,...}:operation) =
let
val arg_typestrs = map (fn a => (Rep_OclType.string_of_OclType o #2 )a )
@ -1301,7 +1304,9 @@ fun class_of (name:Path) (cl:Classifier list):Classifier = hd (filter (fn a => i
then true else false ) cl )
handle _ => error ("class_of: class "^(string_of_path name)^" not found!\n")
fun parent_of C cl = (class_of (parent_name_of C) cl)
fun parents_of C cl =
@ -1311,6 +1316,7 @@ fun parents_of C cl =
then [(name_of OclAnyC)]
else [class]@(parents_of (class_of class cl) cl)))
(* returns the activity graphs (list) of the given Classifier --> this is a list of StateMachines*)
(* Classifier -> ActivityGraph list *)
fun activity_graphs_of (Class{activity_graphs,...}) = activity_graphs

4
su4sml/src/test-suite.sml
View File

@ -128,13 +128,13 @@ val testcases = [
uml = prefix^"vehicles/vehicles.zargo",
ocl = prefix^"vehicles/vehicles.ocl",
result = initResult
}:testcase,
}:testcase (*,
{
name = "SimpleChair",
uml = prefix^"SimpleChair/SimpleChair.zargo",
ocl = "",
result = initResult
}:testcase
}:testcase *)
]

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

@ -1,64 +0,0 @@
(*****************************************************************************
* 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

148
su4sml/src/wfcpo-gen/command_query_consistency.sml Normal file
View File

@ -0,0 +1,148 @@
(*****************************************************************************
* 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 COMMAND_QUERY_CONSTRAINT =
sig
val ops_are_query : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
val ops_are_command : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
end
structure Command_Query_Constraint:COMMAND_QUERY_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
(* oclparser *)
open Ext_Library
open ModelImport
(* wfcpo-gen *)
open WFCPOG_Library
open WFCPO_Naming
exception WFCPO_QueryCommandError of string
fun post_implies_args_and_self_at_pre oper class =
let
val posts = List.map (fn (a,b) => b) (postcondition_of_op oper)
val fst = conjugate_terms posts
val args = arguments_of_op oper
val args2term = List.map (fn (a,b) => Variable(a,b)) args
val arg_terms = List.map (fn a =>
let
val ta = type_of_term a
val x = OperationCall (a,ta,["oclLib","OclAny","atPre"],[],ta)
in
OperationCall (a,ta,["oclLib","Boolean","="],[(x,type_of_term x)],Boolean)
end
) args2term
val selft = type_of class
val self = Variable("self",selft)
val self_term_help = OperationCall (self,selft,["oclLib","OclAny","atPre"],[],selft)
val self_term = OperationCall (self,selft,["oclLib","OclAny","="],[(self_term_help,type_of_term self_term_help)],Boolean)
val snd = conjugate_terms (self_term::arg_terms)
in
OperationCall(fst,Boolean,["oclLib","Boolean","implies"],[(snd,Boolean)],Boolean)
end
fun post_implies_not_args_or_not_self_at_pre oper class =
let
val posts = List.map (fn (a,b) => b) (postcondition_of_op oper)
val fst = conjugate_terms posts
val args = arguments_of_op oper
val args2term = List.map (fn (a,b) => Variable(a,b)) args
val arg_terms = List.map (fn a =>
let
val ta = type_of_term a
val x = OperationCall (a,ta,["oclLib","OclAny","atPre"],[],ta)
in
OperationCall (a,ta,["oclLib","OclAny","<>"],[(x,type_of_term x)],Boolean)
end
) args2term
val selft = type_of class
val self = Variable("self",selft)
val self_term_help = OperationCall (self,selft,["oclLib","OclAny","atPre"],[],selft)
val self_term = OperationCall (self,selft,["oclLib","OclAny","<>"],[(self_term_help,type_of_term self_term_help)],Boolean)
val snd = disjugate_terms (self_term::arg_terms)
in
OperationCall(fst,Boolean,["oclLib","Boolean","implies"],[(snd,Boolean)],Boolean)
end
fun ops_are_query_help [] model = []
| ops_are_query_help (h::classes) (model as (clist,alist)) =
let
val qops = query_operations_of h
val x = List.map (fn a => (post_implies_args_and_self_at_pre a h)) qops
in
(x)@(ops_are_query_help classes model)
end
fun ops_are_command_help [] model = []
| ops_are_command_help (h::classes) (model as (clist,alist)) =
let
val cops = command_operations_of h
val x = List.map (fn a => (post_implies_not_args_or_not_self_at_pre a h)) cops
in
(x)@(ops_are_command_help classes model)
end
fun ops_are_query wfpo (model:Rep.Model as (clist,alist)) =
let
val class = removeOclLibrary clist
in
ops_are_query_help class model
end
fun ops_are_command wfpo (model:Rep.Model as (clist,alist)) =
let
val class = removeOclLibrary clist
in
ops_are_command_help class model
end
end;

63
su4sml/src/wfcpo-gen/constructor_consistency.sml
View File

@ -42,11 +42,16 @@
(** 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
(** sub constraint, included in constructor consistency.*)
val overwrites_old_creators : Rep.Model -> bool
(** sub constraint, included in constructor consistency.*)
val attributes_are_inited : Rep.Model -> bool
(** Any kind of Exception *)
exception WFCPO_ConstructorError of string
end
functor Constructor_Constraint (SuperCon : BASE_CONSTRAINT) : CONSTRUCTOR_CONSTRAINT =
structure Constructor_Constraint : CONSTRUCTOR_CONSTRAINT =
struct
(* SU4SML *)
@ -61,24 +66,12 @@ 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
open WFCPOG_Library
exception WFCPO_ConstructorError of string
(* 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
@ -116,11 +109,37 @@ fun post_implies_invariant (model as (clist, alist)) =
post_implies_invariant_help class model
end
fun generate_po (model as (clist,alist)) =
fun overwrites_old_creators_help [] model = [true]
| overwrites_old_creators_help (h::class) (model as (clist,alist)) =
let
val x1 = post_implies_invariant model
val crea = creation_operations_of (name_of h) model
val over_ops = modified_operations_of (name_of h) model
in
x1
(List.all (fn a => List.exists (fn b => b =a) (over_ops)) crea)::(overwrites_old_creators_help class model)
end
end;
fun overwrites_old_creators (model as (clist, alist)) =
let
val class = removeOclLibrary clist
in
List.all (fn a => a) (overwrites_old_creators_help class model)
end
fun attributes_are_inited_help [] model = [true]
| attributes_are_inited_help (h::class) (model as (clist,alist)) =
let
val attrs = attributes_of h
fun inited NONE = false
| inited (SOME(x)) = true
in
(List.all (fn a => inited (#init a)) (attrs))::(attributes_are_inited_help class model)
end
fun attributes_are_inited (model as (clist,alist)) =
let
val class = removeOclLibrary clist
in
List.all (fn a => a) (attributes_are_inited_help class model)
end
end;

35
su4sml/src/wfcpo-gen/data_model_consistency.sml
View File

@ -42,13 +42,12 @@
(** 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
(** sub constraint, included in liskov.*)
val class_model_consistency : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in liskov.*)
val strong_model_consistency : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Data_Model_Consistency_Constraint (SuperCon : BASE_CONSTRAINT) : BASE_CONSTRAINT =
structure Data_Model_Consistency_Constraint : DATA_MODEL_CONSISTENCY_CONSTRAINT =
struct
(* su4sml *)
@ -64,13 +63,11 @@ open ModelImport
open Context
(* wfcpo-gen *)
open WFCPO_Library
open WFCPOG_Library
exception ConstraintError of string
exception BaseConstraintError of string
exception LiskovError of string
type constraint = SuperCon.constraint
exception WFCPO_DataModelError
fun c_allInstance_term (c:Classifier) =
let
@ -84,7 +81,7 @@ fun c_allInstance_term (c:Classifier) =
val term = add_source (class,allInstances)
val term = add_source (allInstances,exists)
in
OperationCall (term,DummyT,["holOclLib","Boolean","OclLocalValid"],[],Boolean)
OperationCall (term,type_of_term term,["holOclLib","Boolean","OclLocalValid"],[(Variable("tau",DummyT),DummyT)],Boolean)
end
(* E t. t |= c::allInstances()->exists(x|x.oclIsTypeOf(c)) *)
@ -100,7 +97,7 @@ 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)) =
fun class_model_consistency wfpo (model as (clist,alist)) =
let
val classifiers = removeOclLibrary (clist)
in
@ -112,22 +109,14 @@ fun strong_model_consistency_help classes model =
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)
[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)) =
fun strong_model_consistency wfpo (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;

77
su4sml/src/wfcpo-gen/core.sml → su4sml/src/wfcpo-gen/datatab.sml
View File

@ -2,10 +2,10 @@
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* context_declarations.sml ---
* datatab.sml --- a very simplistic datatab implementation
* This file is part of su4sml.
*
* Copyright (c) 2005-2007, ETH Zurich, Switzerland
* Copyright (c) 2008 Achim D. Brucker, Germany
*
* All rights reserved.
*
@ -37,28 +37,57 @@
* (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 $ *)
(* $Id: wfcpog.sml 7256 2008-02-10 19:31:53Z 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")
A simple Object Type (similar to the one used in Isabelle) for
fooling the type system of SML.
*)
end;
structure Object = struct type T = exn end;
(**
A very simplistic table using integers as key. The signature is a
subset of the TableFun provided by Isabelle, i.e., when using a
Isabelle based setup, 'a Datatab can be implemented/replaced
by
structure Datatab = TableFun(type key = int val ord = int_ord);
*)
signature DATATAB =
sig
type 'a table
type key
exception DUP of key
exception SAME of key
exception UNDEF of key
val empty : 'a table
val keys : 'a table -> key list
val lookup : 'a table -> key -> 'a option
val update : key * 'a -> 'a table -> 'a table
end
structure Datatab:DATATAB =
struct
type key = int
type 'a table = (key * 'a) list
exception DUP of key
exception SAME of key
exception UNDEF of key
val empty=[]
(* 'a option *)
fun lookup t k = case (List.filter (fn (k',v) => (k'=k)) t) of
[] => NONE
| t' => SOME ((#2 o hd) t')
(* 'a table *)
fun update (k,v) [] = [(k,v)]
| update (k,v) (x::xs) = if (#1 x) = k
then raise DUP k (* (k,v)::xs *)
else x::(update (k,v) xs)
(* key list *)
fun keys (t:'a table) = map (#1) t
end

24
su4sml/src/wfcpo-gen/example.sml Normal file
View File

@ -0,0 +1,24 @@
open WFCPOG_Registry
open WFCPOG_Constraint_Library
(* GET BASE CONSTRAINT *)
val tax = get_wfpo supported "tax"
val rfm_syn = get_wfpo supported "rfm_syn"
(* EXTEND BASE CONSTRAINT WITH ADDITIONAL DATA *)
(* MAXIMUM DEPTH OF THE INHERITANCE STRUCTURE *)
val md0 = TAX_Data.put ({key=9,max_depth=0}) tax
val md1 = TAX_Data.put ({key=9,max_depth=1}) tax
val md2 = TAX_Data.put ({key=9,max_depth=2}) tax
val md3 = TAX_Data.put ({key=9,max_depth=3}) tax
val md4 = TAX_Data.put ({key=9,max_depth=4}) tax
val md5 = TAX_Data.put ({key=9,max_depth=5}) tax
val md6 = TAX_Data.put ({key=9,max_depth=6}) tax
val md7 = TAX_Data.put ({key=9,max_depth=7}) tax
val md8 = TAX_Data.put ({key=9,max_depth=8}) tax
(* REFINEMENT OF PACKAGES *)
val sc1 = RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair01"],["ConcreteSimpleChair01"])]}) rfm_syn
val sc2 = RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair02"],["ConcreteSimpleChair02"])]}) rfm_syn
val sc3 = RFM_Data.put ({key=10,rfm_tuples=[(["AbstractSimpleChair01"],["ConcreteSimpleChair01"]),(["AbstractSimpleChair02"],["ConcreteSimpleChair02"])]}) rfm_syn

124
su4sml/src/wfcpo-gen/interface_consistency.sml Normal file
View File

@ -0,0 +1,124 @@
(*****************************************************************************
* 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 INTERFACE_CONSTRAINT =
sig
val has_consistent_stereotypes : WFCPOG.wfpo -> Rep.Model -> bool
val is_nameclash_free : WFCPOG.wfpo -> Rep.Model -> bool
end
structure Interface_Constraint:INTERFACE_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
(* oclparser *)
open Ext_Library
open ModelImport
(* wfcpo-gen *)
open WFCPOG_Library
open WFCPO_Naming
exception WFCPOG_InterfaceError of string
fun list_has_dup [] = false
| list_has_dup [x] = false
| list_has_dup (h::tail) =
if List.exists (fn a => a = h) tail
then false
else list_has_dup (tail)
fun has_consistent_stereotypes_help [] model = true
| has_consistent_stereotypes_help ((Interface{operations,...})::classes) (model as (clist,alist)) =
List.all (fn a => not (List.exists (fn b => (b = "create") orelse (b = "destroy")) (#stereotypes a))) (operations)
| has_consistent_stereotypes_help (h::classes) model = has_consistent_stereotypes_help classes model
fun is_nameclash_free_help [] model = true
| is_nameclash_free_help ((Class{interfaces,...})::classes) (model as (clist,alist)) =
if (List.length(interfaces)) <= 1
then is_nameclash_free_help classes model
else
let
val if_list = List.map (fn a => class_of_type a model) interfaces
val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of (name_of a) model))) if_list)
in
list_has_dup (op_name_list)
end
| is_nameclash_free_help ((AssociationClass{interfaces,...})::classes) (model as (clist,alist)) =
if (List.length(interfaces)) <= 1
then is_nameclash_free_help classes model
else
let
val if_list = List.map (fn a => class_of_type a model) interfaces
val op_name_list = List.concat (List.map (fn a => (List.map (name_of_op) (all_operations_of (name_of a) model))) if_list)
in
list_has_dup (op_name_list)
end
| is_nameclash_free_help (x::classes) model = is_nameclash_free_help classes model
fun has_consistent_stereotypes wfpo (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
in
has_consistent_stereotypes_help classes model
end
fun is_nameclash_free wfpo (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
in
is_nameclash_free_help classes model
end
end;

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

@ -1,20 +0,0 @@
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

185
su4sml/src/wfcpo-gen/library.sml
View File

@ -13,7 +13,8 @@
* 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 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
@ -43,7 +44,7 @@
* 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 =
signature WFCPOG_LIBRARY =
sig
(** Get the name of a certain precondition.*)
@ -58,16 +59,28 @@ sig
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
(** *)
val disjugate_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
(** Get an attribute by name. *)
val get_attribute : string -> Rep_Core.Classifier -> Rep.Model -> Rep_Core.attribute
(** Get an operation by name. *)
val get_operation : string -> Rep_Core.Classifier -> Rep.Model -> 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
(** *)
val class_has_local_op : string -> Rep.Model -> Rep_Core.Classifier -> bool
(** *)
val class_of_package : Rep_OclType.Path -> Rep.Model -> Rep_Core.Classifier list
(** Get all query operations of a classifier.*)
val query_operations_of : Rep_Core.Classifier -> Rep_Core.operation list
(** Get all command operations of a classifier.*)
val command_operations_of : Rep_Core.Classifier -> Rep_Core.operation list
(** 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.*)
@ -79,7 +92,17 @@ sig
(** 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
val destruction_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all public operations of a classifier.*)
val public_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all private operations of a classifier.*)
val private_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all package operations of a classifier.*)
val package_operations_of : Rep_OclType.Path -> Rep.Model -> Rep_Core.operation list
(** Get all protected operations of a classifier.*)
val protected_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.*)
@ -94,10 +117,14 @@ sig
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
(** Substitute (string,Type) args as (Variable(s,Type),Type) args.*)
val args2varargs : (string * Rep_OclType.OclType) list -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType) list
(** Add self as argument *)
val selfarg : Rep_OclType.OclType -> (Rep_OclTerm.OclTerm * Rep_OclType.OclType)
(** Any kind of exceptions. *)
exception WFCPO_LibraryError of string
exception WFCPOG_LibraryError of string
end
structure WFCPO_Library:WFCPO_LIBRARY =
structure WFCPOG_Library:WFCPOG_LIBRARY =
struct
(* SU4SML *)
@ -107,15 +134,15 @@ open Rep_OclType
open Rep_OclTerm
open OclLibrary
open Rep2String
open XMI_DataTypes
(* OclParser *)
open Ext_Library
(* WFCPO-Gen *)
open WFCPO_Naming
open Base_Constraint
exception WFCPO_LibraryError of string
exception WFCPOG_LibraryError of string
fun name_of_precondition ((a:string option),(t:OclTerm)) = a
@ -127,21 +154,33 @@ 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")
fun conjugate_terms [] = raise WFCPOG_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")
then (OperationCall(h,type_of_term h,["oclLib","Boolean","and"],[(x,type_of_term x)],Boolean))
else raise WFCPOG_LibraryError ("type of term is not Boolean. \n")
end
fun disjugate_terms [] = raise WFCPOG_LibraryError("Empty list not disjugateable. \n")
| disjugate_terms [x:OclTerm] = (x)
| disjugate_terms ((h:OclTerm)::tail) =
let
val x = disjugate_terms tail
in
if (type_of_term h = Boolean)
then (OperationCall(h,type_of_term h,["oclLib","Boolean","or"],[(x,type_of_term x)],Boolean))
else raise WFCPOG_LibraryError ("type of term is not Boolean. \n")
end
(* create normal list from a list of options type *)
@ -157,14 +196,6 @@ 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 *)
@ -200,11 +231,24 @@ fun sig_conforms_to [] [] model = true
result
end
fun query_operations_of (Class{operations,...}) = List.filter (fn a => (#isQuery a)) operations
| query_operations_of (AssociationClass{operations,...}) = List.filter (fn a => (#isQuery a)) operations
| query_operations_of (Primitive{operations,...}) = List.filter (fn a => (#isQuery a)) operations
| query_operations_of (Interface{operations,...}) = List.filter (fn a => (#isQuery a)) operations
| query_operations_of x = []
fun command_operations_of (Class{operations,...}) = List.filter (fn a => not (#isQuery a)) operations
| command_operations_of (AssociationClass{operations,...}) = List.filter (fn a => not (#isQuery a)) operations
| command_operations_of (Primitive{operations,...}) = List.filter (fn a => not (#isQuery a)) operations
| command_operations_of (Interface{operations,...}) = List.filter (fn a => not (#isQuery a)) operations
| command_operations_of x = []
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
@ -215,8 +259,22 @@ fun class_contains_op oper model classifier =
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))
and local_operations_of c_name model =
let
val class = class_of_type (path_to_type c_name) model
in
(operations_of class)
end
fun class_has_local_op name model classifier =
let
val ops = local_operations_of (name_of classifier) model
in
List.exists (fn a => (#name a) = name) ops
end
fun embed_local_operation oper [] model = [oper]
| embed_local_operation lop ((oper:operation)::iops) model =
@ -237,10 +295,14 @@ fun embed_local_operations [] iops model = iops
(* 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 class = class_of_type (path_to_type c_name) model
val _ = trace 50 ("inh ops 1: classifier = " ^ (classifier2string class) ^ "\n")
val parents = parents_of class (#1 model)
val c_parents = List.map (fn a => class_of a (#1 model)) parents
val _ = trace 50 ("inh ops 2\n")
val c_parents = List.map (fn a => class_of_type (path_to_type a) model) parents
val _ = trace 50 ("inh ops 3\n")
val ops_of_par = (List.map (operations_of) c_parents)
val _ = trace 50 ("inh ops 4\n")
in
List.foldr (fn (a,b) => embed_local_operations a b model) (List.last (ops_of_par)) ops_of_par
end
@ -249,7 +311,9 @@ fun inherited_operations_of c_name (model as (clist,alist)) =
fun all_operations_of c_name model =
let
val lo = local_operations_of c_name model
val _ = trace 50 ("all ops 1\n")
val io = inherited_operations_of c_name model
val _ = trace 50 ("all ops 2\n")
in
embed_local_operations lo io model
end
@ -290,6 +354,57 @@ fun destruction_operations_of c_name (model:Rep.Model) =
creators
end
fun public_operations_of c_name (model:Rep.Model) =
let
val ops = all_operations_of c_name model
in
List.filter (fn a => (#visibility a) = public) ops
end
fun private_operations_of c_name (model:Rep.Model) =
let
val ops = all_operations_of c_name model
in
List.filter (fn a => (#visibility a) = private) ops
end
fun package_operations_of c_name (model:Rep.Model) =
let
val ops = all_operations_of c_name model
in
List.filter (fn a => (#visibility a) = package) ops
end
fun protected_operations_of c_name (model:Rep.Model) =
let
val ops = all_operations_of c_name model
in
List.filter (fn a => (#visibility a) = protected) ops
end
fun get_operation s classifier model =
let
val _ = trace 100 ("get_operation: \n")
val x = List.find (fn a => if (name_of_op a = s) then true else false) (all_operations_of (name_of classifier) model)
val _ = trace 100 ("end get_operation\n")
in
case x of
NONE => raise WFCPOG_LibraryError ("No operation found using 'get_operation'.\n")
| SOME (x) => x
end
fun get_attribute s classifier model =
let
val x = List.find (fn a => if ((#name a) = s) then true else false) (attributes_of classifier)
in
case x of
NONE => raise WFCPOG_LibraryError ("No operation found using 'get_attribute'.\n")
| SOME (x) => x
end
fun go_up_hierarchy location func (model as (clist,alist)) =
let
val parent = parent_of location (#1 model)
@ -298,7 +413,7 @@ fun go_up_hierarchy location func (model as (clist,alist)) =
then parent
else
(if (type_of parent = OclAny)
then raise WFCPO_LibraryError ("No such property using 'go_up_hierarchy'.\n")
then raise WFCPOG_LibraryError ("No such property using 'go_up_hierarchy'.\n")
else go_up_hierarchy parent func model
)
end
@ -338,18 +453,26 @@ fun all_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")
| rel_path_of [x] [y] = if (x=y) then [] else raise WFCPOG_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 WFCPOG_LibraryError ("rel_path_of only possible for name with same package/prefix")
| rel_path_of pkg name =
if (List.hd(pkg) = List.hd(name)) then (rel_path_of (List.tl pkg) (List.tl name)) else raise WFCPOG_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")
fun substitute_package [] tpackage [] = raise WFCPOG_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 x tpackage [] = raise WFCPOG_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)
fun class_of_package pkg (model as (clist,alist)) =
List.filter (fn a => package_of a = pkg) clist
fun args2varargs [] = []
| args2varargs ((a,b)::tail) = (Variable(a,b),b)::(args2varargs tail)
fun selfarg typ = (Variable("self",typ),typ)
end;

89
su4sml/src/wfcpo-gen/liskov_constraint.sml
View File

@ -42,41 +42,67 @@
(** 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
type Liskov_args
structure LSK_Data :
sig
type T = Liskov_args
val get : WFCPOG.wfpo -> T
val put : T -> WFCPOG.wfpo -> WFCPOG.wfpo
val map : (T -> T) -> WFCPOG.wfpo -> WFCPOG.wfpo
end
val print_liskov_args : Liskov_args -> unit
(** sub constraint, included in liskov.*)
val weaken_precondition : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in liskov.*)
val strengthen_postcondition : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in liskov.*)
val conjugate_invariants : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Liskov_Constraint (SuperCon : BASE_CONSTRAINT) : LISKOV_CONSTRAINT =
structure Liskov_Constraint : LISKOV_CONSTRAINT =
struct
exception WFCPOG_LiskovError of string
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
(* oclparser *)
open Ext_Library
open ModelImport
open Rep2String
(* wfcpo-gen *)
open WFCPO_Library
open WFCPOG_Library
open WFCPO_Naming
open Datatab
exception WFCPO_LiskovError of string
exception ConstraintError of string
exception BaseConstraintError of string
exception LiskovError of string
type constraint = SuperCon.constraint
type Liskov_args = {
model:string,
size:int
}
structure LSK_Data = WfpoDataFun
(struct
type T = Liskov_args;
val empty = ({model="", size=0});
fun copy T = T;
fun extend T = T;
end);
fun print_liskov_args (args:Liskov_args) =
print (concat["Lisov with args: size=\"",Int.toString (#size args), "\""," and model=\"", #model (args),"\"\n\n"])
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 op_of_super = get_operation (name_of_op oper) super_class model
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
@ -92,9 +118,9 @@ fun generate_return_value typ oper sub_class super_class model =
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))
val term_super = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,[(generate_opt_name "gen_pre" a)],(args2varargs (arguments_of_op op_of_super))))) (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))
val term_sub = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,[(generate_opt_name "gen_pre" a)],(args2varargs (arguments_of_op oper))))) (precondition_of_op oper))
in
OperationCall(term_super,Boolean,["Boolean","implies"],[(term_sub,type_of_term term_sub)],Boolean)
end
@ -110,13 +136,13 @@ fun generate_return_value typ oper sub_class super_class model =
| 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))
val term_sub = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,[(generate_opt_name "gen_post" a)],(args2varargs (arguments_of_op oper))))) (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))
val term_super = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,[(generate_opt_name "gen_post" a)],(args2varargs (arguments_of_op op_of_super))))) (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")
| x => raise WFCPO_LiskovError ("Wrong Argument for generate_return_value. Only 1 (pre) and 2 (post) allowed.\n")
end
@ -132,7 +158,7 @@ fun weaken_precondition_help [] model = []
pos@(weaken_precondition_help clist model)
end
fun weaken_precondition (model as (clist,alist)) =
fun weaken_precondition wfpo (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
@ -152,7 +178,7 @@ fun strengthen_postcondition_help [] model = []
pos@(strengthen_postcondition_help clist model)
end
fun strengthen_postcondition (model as (clist,alist)) =
fun strengthen_postcondition wfpo (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
@ -165,7 +191,7 @@ fun conjugate_invariants_help [] model = []
(* 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
val invs = List.map (fn (a,b) => Predicate(b,type_of_term b,[(generate_opt_name "inv" a)],[selfarg (type_of class)])) invariants
in
if (List.length(invs) = 0)
then (conjugate_invariants_help clist model)
@ -173,22 +199,23 @@ fun conjugate_invariants_help [] model = []
(conjugate_terms invs)::(conjugate_invariants_help clist model)
end
fun conjugate_invariants (model as (clist,alist)) =
fun conjugate_invariants wfpo (model as (clist,alist)) =
let
val cl = removeOclLibrary clist
in
conjugate_invariants_help cl model
end
fun generate_po (model as (clist,alist)) =
fun generate_po (model as (clist,alist)) data =
let
val _ = trace zero ("generate_po: \n")
val _ = trace zero ("weaken the precondition.\n")
val x1 = weaken_precondition model
val x1 = weaken_precondition model data
val _ = trace zero ("strengthen the postcondition.\n")
val x2 = strengthen_postcondition model
val x2 = strengthen_postcondition model data
val _ = trace zero ("conjugate the invariants.\n")
val x3 = conjugate_invariants model
val x3 = conjugate_invariants model data
in
x1@x2@x3
end

17
su4sml/src/wfcpo-gen/init-test-setup.sml → su4sml/src/wfcpo-gen/load_model.sml
View File

@ -8,20 +8,23 @@ open Ext_Library
(* WFCPO-GEN *)
open WFCPO_Library
open WFCPO_Registry
(* set debugging settings *)
val _ = Control.Print.printDepth:=10
val _ = Control.Print.printDepth:=20
val _ = Control.Print.printLength:=30
(*
val zargo = "../../../stack_manu/stack.zargo"
val ocl = "../../../stack_manu/stack.ocl"
*)
val zargo = "../../../examples/ebank/ebank.zargo"
val ocl="../../../examples/ebank/ebank.ocl"
val zargo = "../../../examples/calendar/calendar.zargo"
val ocl="../../../examples/calendar/calendar.ocl"
(** impor model *)
(** import model *)
val i_model = import zargo ocl []
val (clist,alist) = normalize_ext i_model
val model = ((clist@oclLib),(alist))
val classifiers = removeOclLibrary clist

83
su4sml/src/wfcpo-gen/old_registry.sml Normal file
View File

@ -0,0 +1,83 @@
signature WFCPO_REGISTRY =
sig
datatype constraint =
Liskov of
{
(** subconstraint *)
weaken_pre : bool,
(** subconstraint *)
strengthen_post : bool,
(** subconstraint *)
conjugate_inv : bool
}
| DataModel of
{
(** subconstraint *)
class_model_con : bool,
(** subconstraint *)
strong_model_con : bool
}
| Refine of
{
(** argument *)
abs_rel : string list list
}
val generate_po : constraint -> Rep.Model -> Rep_OclTerm.OclTerm list
val analyze_model : constraint list -> Rep.Model -> Rep_OclTerm.OclTerm list
end;
structure WFCPO_Registry : WFCPO_REGISTRY =
struct
datatype constraint =
Liskov of
{
weaken_pre : bool,
strengthen_post : bool,
conjugate_inv : bool
}
| DataModel of
{
class_model_con : bool,
strong_model_con : bool
}
| Refine of
{
abs_rel : string list list
}
fun generate_po (Liskov{weaken_pre,strengthen_post,conjugate_inv}) model =
let
val wp = if (weaken_pre)
then Liskov_Constraint.weaken_precondition model
else []
val sp = if (strengthen_post)
then Liskov_Constraint.strengthen_postcondition model
else []
val ci = if (conjugate_inv)
then Liskov_Constraint.conjugate_invariants model
else []
in
wp@sp@ci
end
| generate_po (DataModel{class_model_con,strong_model_con}) model =
let
val cmc = if (class_model_con)
then Data_Model_Consistency_Constraint.class_model_consistency model
else []
val smc = if (strong_model_con)
then Data_Model_Consistency_Constraint.strong_model_consistency model
else []
in
cmc@smc
end
| generate_po (Refine {abs_rel}) model = []
fun analyze_model [] model = []
| analyze_model [x:constraint] model = generate_po x model
| analyze_model (con_list) model = List.concat (List.map (fn a => generate_po a model) con_list)
end

203
su4sml/src/wfcpo-gen/operational_consistency.sml
View File

@ -42,16 +42,18 @@
(** 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
val generate_secureUML_creators_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in operational consistency.*)
val generate_operation_constraints : Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_destructors_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
(** sub constraint, included in operational consistency.*)
val generate_attribute_constraints : Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_getters_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_setters_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_secureUML_op_sec_po : Rep_Core.Classifier -> Rep.Model -> Rep_OclTerm.OclTerm list
val generate_pos : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
end
functor Operational_Constraint (SuperCon : BASE_CONSTRAINT) : OPERATIONAL_CONSTRAINT =
structure Operational_Constraint : OPERATIONAL_CONSTRAINT =
struct
@ -67,64 +69,171 @@ open ModelImport
(* WFCPO *)
open WFCPO_Naming
open WFCPO_Library
open WFCPOG_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
exception WFCPO_OperationalError
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)) =
fun case_insensitive "" = ""
| case_insensitive s:string =
let
val classes = removeOclLibrary clist
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
(* get corresponding operation x from x_sec of. *)
fun secureUML_real_op oper class model =
let
val name = name_of_op oper
val len = String.size name
val substr = String.substring (name,0,len-4)
in
generate_class_constraints_help classes model
get_operation substr class model
end
fun generate_operation_constraints (model as (clist,alist)) =
fun secureUML_sec_op oper class model =
let
val classes = removeOclLibrary clist
val name = name_of_op oper ^ "_sec"
in
generate_operation_constraints_help classes model
get_operation name class model
end
fun generate_attribute_constraints (model as (clist,alist)) =
fun secureUML_get_att_name oper =
let
val classes = removeOclLibrary clist
val name = name_of_op oper
val len = String.size name
in
generate_attribute_constraints_help classes model
String.substring (name,0,len-4)
end
(* *)
fun secureUML_getter_operations_of class_n model = List.filter (fn a => String.isPrefix "get" (name_of_op a)) (local_operations_of class_n model)
(* *)
fun secureUML_setter_operations_of class_n model = List.filter (fn a => String.isPrefix "set" (name_of_op a)) (local_operations_of class_n model)
(* *)
fun secureUML_op_sec_operations_of class_n model = List.filter (fn a => String.isSuffix "_sec" (name_of_op a)) (local_operations_of class_n model)
fun secureUML_substitute_terms (OperationCall(src,typ,path,args,rtyp)) class =
let
val op_name = List.last path
val p_len = List.length path
val p = List.take (path,p_len-1)
in
if (name_of class) = p
then (* substitute operation x with x_sec *)
(OperationCall(src,typ,p@[op_name^"_sec"],args,rtyp))
else OperationCall(src,typ,path,args,rtyp)
end
| secureUML_substitute_terms (AttributeCall(src,typ,path,rtyp)) class =
let
val att_name = List.last path
val p_len = List.length path
val p = List.take (path,p_len-1)
in
if (name_of class) = p
then (* substitute attribute x with operation getX() *)
OperationCall(src,typ,p@["get"^att_name],[],rtyp)
else AttributeCall(src,typ,path,rtyp)
end
| secureUML_substitute_terms x class = x
fun generate_secureUML_creators_po class (model as (clist,alist)) =
let
val creators = creation_operations_of (name_of class) model
in
(List.map (fn a =>
let
val op_res = result_of_op a
val result = Variable("result",op_res)
val term1 = OperationCall(result,op_res,(name_of class)@["oclIsUndefined"],[],Boolean)
val term2 = OperationCall(result,op_res,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
end
) creators)
end
fun generate_secureUML_destructors_po class (model as (clist,alist)) =
let
val destructors = destruction_operations_of (name_of class) model
in
(List.map (fn a =>
let
val self = Variable("self",type_of class)
val term1 = OperationCall(self,type_of class,(name_of class)@["oclIsUndefined"],[],Boolean)
val atPre = OperationCall(self,type_of class,["oclLib","OclAny","atPre"],[],type_of class)
val term2 = OperationCall(atPre,type_of class,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
end
) destructors)
end
fun generate_secureUML_getters_po class (model as (clist,alist)) =
let
val getter = secureUML_getter_operations_of (name_of class) model
in
(List.map (fn a =>
let
val op_res = result_of_op a
val att_name = secureUML_get_att_name a
val result = Variable("result",op_res)
val self = Variable("self",type_of class)
val atCall = AttributeCall(self,type_of class,(name_of class)@[(att_name)],op_res)
in
OperationCall(result,op_res,["oclLib","Boolean","="],[(atCall,op_res)],Boolean)
end
) getter)
end
fun generate_secureUML_setters_po class (model as (clist,alist)) =
let
val setter = secureUML_setter_operations_of (name_of class) model
in
(List.map (fn a =>
let
val (name,arg_type)= hd(arguments_of_op a)
val self = Variable("self",type_of class)
val att_name = secureUML_get_att_name a
val arg = Variable(name,arg_type)
val att = AttributeCall(self,type_of class,(name_of class)@[att_name],arg_type)
val term1 = OperationCall(att,arg_type,["oclLib","Boolean","="],[(arg,arg_type)],Boolean)
val term2 = OperationCall(att,arg_type,(name_of class)@["modifiedOnly"],[],Boolean)
in
OperationCall(term1,Boolean,["oclLib","Boolean","and"],[(term2,Boolean)],Boolean)
end
) setter)
end
fun generate_secureUML_op_sec_po class (model as (clist,alist)) =
let
val op_sec = secureUML_op_sec_operations_of (name_of class) model
in
List.concat (List.map (fn a =>
let
val real_op = secureUML_real_op a class model
val add_pres = List.map (fn (a,b) => b ) (precondition_of_op real_op)
val real_posts = postcondition_of_op real_op
val add_posts = List.map (fn (a,b) => secureUML_substitute_terms b class) (real_posts)
in
add_pres@add_posts
end
) op_sec)
end
fun generate_po (model as (clist,alist)) = (* [Variable("s",DummyT)] *)
fun generate_pos wfpo (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 *)
val design_model_classes = removeOclLibrary clist
val po1 = List.map (fn a => generate_secureUML_creators_po a model) design_model_classes
val po2 = List.map (fn a => generate_secureUML_destructors_po a model) design_model_classes
val po3 = List.map (fn a => generate_secureUML_getters_po a model) design_model_classes
val po4 = List.map (fn a => generate_secureUML_setters_po a model) design_model_classes
val po5 = List.map (fn a => generate_secureUML_op_sec_po a model) design_model_classes
in
List.concat(po1@po2@po3@po4@po5)
end
end;

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

@ -1,30 +0,0 @@
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;

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

@ -1,12 +1,20 @@
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
type RFM_args
exception RefineError of string
structure RFM_Data :
sig
type T = RFM_args
val get : WFCPOG.wfpo -> T
val put : T -> WFCPOG.wfpo -> WFCPOG.wfpo
val map : (T -> T) -> WFCPOG.wfpo -> WFCPOG.wfpo
end
val check_syntax : WFCPOG.wfpo -> Rep.Model -> bool
val refine_po : WFCPOG.wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
exception WFCPO_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)
@ -14,7 +22,7 @@ sig
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 *) =
structure Refine_Constraint : REFINE_CONSTRAINT =
struct
(* su4sml *)
@ -27,31 +35,30 @@ open Rep2String
open Ext_Library
(* wfcpo-gen *)
open Base_Constraint
open WFCPO_Library
open WFCPOG_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
exception WFCPO_RefineError of string
val FromPack = ref ["AbstractSimpleChair01"]
val ToPack = ref ["ConcreteSimpleChair01"]
type RFM_args = {
key : int,
rfm_tuples : (Rep_OclType.Path * Rep_OclType.Path) list
}
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
structure RFM_Data = WfpoDataFun
(struct
type T = RFM_args;
val empty = ({key=10,rfm_tuples=[([]:Path,[]:Path)]});
fun copy T = T;
fun extend T = T;
end);
fun rm x [] = []
| rm x [b] = if (x = b) then [] else [b]
@ -103,7 +110,7 @@ fun map_public_classes fromPath toPath (model as (clist,alist)) =
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")
raise WFCPO_RefineError ("Please adjust model...\n")
end
end
@ -127,7 +134,7 @@ fun map_public_ops [] = [[]]
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")
raise WFCPO_RefineError ("Please adjust model...\n")
end
))]
@(map_public_ops tail)
@ -165,7 +172,7 @@ fun map_types [] fP tP model = []
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")
raise WFCPO_RefineError ("Please adjust model...\n")
end
(* name of the arguments *)
val _ = trace zero ("map_types_6: " ^ string_of_path (name_of c1) ^ "\n")
@ -187,7 +194,7 @@ fun map_types [] fP tP model = []
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")
raise WFCPO_RefineError ("Please adjust model...\n")
end
end
) arg_class_name1
@ -196,7 +203,7 @@ fun map_types [] fP tP model = []
(true)::(map_types tail fP tP model)
end
fun check_syntax fromPath toPath (model:Rep.Model as (clist,alist)) =
fun check_syntax_help (model:Rep.Model as (clist,alist)) fromPath toPath =
let
val _ = trace zero ("CHECK SYNTAX ... \n")
(* check public classes of the two packages *)
@ -210,41 +217,116 @@ fun check_syntax fromPath toPath (model:Rep.Model as (clist,alist)) =
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) =
fun check_syntax wfpo (model:Rep.Model as (clist,alist)) =
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 *)
val data = RFM_Data.get wfpo
val packages = (#rfm_tuples data)
in
(* po1@po2@po3 *)
[(Literal("true",Boolean))]
List.all (fn a => a) (List.map (fn a => check_syntax_help model (#1 a) (#2 a)) packages)
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
(* page 13 *)
fun operation_term oper class =
let
val pres = List.map (fn (a,b) => b) (precondition_of_op oper)
val posts = List.map (fn (a,b) => b) (postcondition_of_op oper)
val con_pres = conjugate_terms pres
val con_posts = conjugate_terms posts
val args = List.map (fn (a,b) => Variable(a,b)) (arguments_of_op oper)
val args_term = conjugate_terms args
val result = Variable("result",result_of_op oper)
val pre_term = conjugate_terms [con_pres,Variable("self",type_of class),args_term]
val post_term = conjugate_terms [con_posts,Variable("self",type_of class),args_term,result]
val pre_local = OperationCall(pre_term,Boolean,["holOclLib","Boolean","OclLocalValid"],[(Variable("tau",DummyT),DummyT)],Boolean)
val post_local = OperationCall(post_term,Boolean,["holOclLib","Boolean","OclLocalValid"],[(Variable("tau",DummyT),DummyT)],Boolean)
val final = conjugate_terms [pre_local,post_local]
in
OperationCall(result,result_of_op oper,["holOclLib","Quantor","existence"],[(final,Boolean)],Boolean)
end
(*
fun lamdba_operation name class model =
let
(* go up hierarchie where operation is implemented *)
(* (operation of subclass, classifier of super class) *)
val cl = go_up_hierarchy class (class_has_local_op name model) model
val oper = get_operation name cl
in
operation_term oper cl
end
*)
(* evaluation to true or exception *)
(*
fun eval_to_true_or_excep name class model =
let
val S = lambda_operation name class model
val tau = Variable("tau",DummyT)
val delta = Variable("delta",DummyT)
in
OperationCall(term,DummyT,["holOclLib","Boolean","OclLocalValid"],[],Boolean)
end
*)
(* valid pre states *)
(* fun valid_pre_states name class model =
let
val
in
end
*)
(* abs make trans, conc can also *)
(*
fun abs_to_conc_trans op_abs op_conc model =
*)
(* conc make trans, abs terminate in R(conc) *)
(*
fun conc_to_abs_trans op_abs op_conc model =
*)
(* forward simulation *)
(* fun fw_sim op_abs op_conc model =
let
val po1 = abs_to_conc_trans op_abs op_conc model
val po2 = conc_to_abs_trans op_abs op_conc model
in
conjugate_terms [po1,po2]
end
*)
(*
fun refine_operation fc fop_name tc top_name model =
let
val prereq1 = eval_to_true_or_excep fop_name fc model
val prereq2 = valid_pre_states fop_name fc model
val po1 =
val po2 =
in
end
fun refine_classifier fc tc model =
let
val fops_name = List.filter (is_visible_op) (all_operations_of fc)
val tops_name = List.filter (is_visible_op) (all_operations_of tc)
val gops = group_op fops tops
in
List.map (fn (a,b) => refine_operation fc (name_of_op a) tc (name_of_op b)) (gops)
end
*)
fun refine_po wfpo (model as (clist,alist)) = []
(*
let
val fc = List.filter (is_visible_cl) (class_of_package from model)
val tc = List.filter (is_visible_cl) (class_of_package to model)
val gc = group_cl fc tc model
in
[]
List.map (fn (a,b) => refine_classifier a b model) gc
end
*)
end;

227
su4sml/src/wfcpo-gen/registry.sml
View File

@ -1,154 +1,83 @@
(*****************************************************************************
* 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 =
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
datatype constraint =
Liskov of
{
(** subconstraint *)
weaken_pre : bool,
(** subconstraint *)
strengthen_post : bool,
(** subconstraint *)
conjugate_inv : bool
}
| DataModel of
{
(** subconstraint *)
class_model_con : bool,
(** subconstraint *)
strong_model_con : bool
}
| Refine of
{
(** argument *)
abs_rel : string list list
}
val generate_po : constraint -> Rep.Model -> Rep_OclTerm.OclTerm list
val analyze_model : constraint list -> Rep.Model -> Rep_OclTerm.OclTerm list
end;
structure WFCPO_Registry : WFCPO_REGISTRY =
struct
datatype constraint =
Liskov of
{
weaken_pre : bool,
strengthen_post : bool,
conjugate_inv : bool
}
| DataModel of
{
class_model_con : bool,
strong_model_con : bool
}
| Refine of
{
abs_rel : string list list
}
fun generate_po (Liskov{weaken_pre,strengthen_post,conjugate_inv}) model =
let
val wp = if (weaken_pre)
then Liskov_Constraint.weaken_precondition model
else []
val sp = if (strengthen_post)
then Liskov_Constraint.strengthen_postcondition model
else []
val ci = if (conjugate_inv)
then Liskov_Constraint.conjugate_invariants model
else []
in
wp@sp@ci
end
| generate_po (DataModel{class_model_con,strong_model_con}) model =
let
val cmc = if (class_model_con)
then Data_Model_Consistency_Constraint.class_model_consistency model
else []
val smc = if (strong_model_con)
then Data_Model_Consistency_Constraint.strong_model_consistency model
else []
in
cmc@smc
end
| generate_po (Refine {abs_rel}) model = []
fun analyze_model [] model = []
| analyze_model [x:constraint] model = generate_po x model
| analyze_model (con_list) model = List.concat (List.map (fn a => generate_po a model) con_list)
end

4
su4sml/src/wfcpo-gen/root.sml Normal file
View File

@ -0,0 +1,4 @@
use "datatab.sml";
use "wfcpog.sml";
use "wfcpog_registry.sml";

117
su4sml/src/wfcpo-gen/syntax_error_db.sml → su4sml/src/wfcpo-gen/taxonomy_consistency.sml
View File

@ -38,50 +38,91 @@
* 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
(** Implementation of the Liskov Substitiution Principle. *)
signature TAXONOMY_CONSTRAINT =
sig
type TAX_args
structure TAX_Data :
sig
type T = TAX_args
val get : WFCPOG.wfpo -> T
val put : T -> WFCPOG.wfpo -> WFCPOG.wfpo
val map : (T -> T) -> WFCPOG.wfpo -> WFCPOG.wfpo
end
val print_taxonomy_args : TAX_args -> unit
(** Subconstraint *)
val has_maxDepth : WFCPOG.wfpo -> Rep.Model -> bool
exception WFCPOG_TaxonomyError of string
end
structure Taxonomy_Constraint:TAXONOMY_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
open XMI_DataTypes
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]
(* oclparser *)
open Ext_Library
open ModelImport
fun add_syntax_error (s:SyntaxError) =
(* wfcpo-gen *)
open WFCPOG_Library
open WFCPO_Naming
open Datatab
exception WFCPOG_TaxonomyError of string
type TAX_args = {
key : int,
max_depth : int
}
structure TAX_Data = WfpoDataFun
(struct
val name =" tax";
type T = TAX_args;
val empty = ({key=0,max_depth=0});
fun copy T = T;
fun extend T = T;
end);
fun print_taxonomy_args (args:TAX_args) =
print (concat["Taxonomy max_Depth with args: max_depth=\"",Int.toString (#max_depth args)," and key", Int.toString(#key args),"\n\n\n"])
fun deep_of_classifier x (Class{parent,...}) (model as (clist,alist)) =
(case parent of
NONE => x+1
| SOME(OclAny) => x+1
| SOME(typ) => deep_of_classifier (x+1) (class_of_type typ model) model
)
| deep_of_classifier x y model = raise WFCPOG_TaxonomyError ("Only Classes can check for maxDepth.\n")
fun has_maxDepth_help depth [] model = true
| has_maxDepth_help depth (h::classes) (model as (clist,alist)) =
let
val x = (SOME(s)::(!SE_db))
val d = deep_of_classifier 0 h model
in
SE_db := x
if (d > depth)
then false
else has_maxDepth_help depth classes model
end
fun has_maxDepth wfpo (model as (clist,alist)) =
let
val classes = removeOclLibrary clist
val tax_args = TAX_Data.get wfpo
val depth = (#max_depth tax_args)
in
has_maxDepth_help depth classes model
end
end;

78
su4sml/src/wfcpo-gen/test-setup.sml
View File

@ -13,83 +13,13 @@ open Ext_Library
open WFCPO_Library
open WFCPO_Naming
open WFCPO_Registry
open WFCPO_Constraint_Library
(* 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
val z = analyze_model [Liskov_all,DataModel_cmc,DataModel_smc] model
val w = analyze_model [Constructor_all] model
val y = analyze_model supported_constraints model

193
su4sml/src/wfcpo-gen/test-suite.sml Normal file
View File

@ -0,0 +1,193 @@
open WFCPOG_Registry
open WFCPOG
open OclLibrary
(* set debugging settings *)
val _ = Control.Print.printDepth:=20
val _ = Control.Print.printLength:=30
(************* GET BASE CONSTRAINT *************************)
(** LISKOV CONSTRAINT **)
val lsk = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "lsk"
(** INTERFACE CONSTRAINT **)
val inf = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "inf"
(** DATA MODEL CONSTRAINT **)
val cm = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "class_model"
val sm = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "strong_model"
(** OPERATIONAL CONSTRAINT **)
val om = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "oper_model"
(** COMMAND/QUERY CONSTRAINT **)
val cmd = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "cmd"
val quy = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "quy"
(** VISIBILITY CONSTRAINT **)
val vis = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "vis"
(** REFINEMENT CONSTRAINT **)
val rfm_syn = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "rfm_syn"
(* TAXONOMY CONSTRAINT *)
val tax = WFCPOG_Registry.get_wfpo WFCPOG_Registry.supported "tax"
(************** CREATE STATIC CONSTRAINTS ********************)
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)
val md3 = WFCPOG_Registry.rename_wfpo "md3" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=3}) tax)
val md4 = WFCPOG_Registry.rename_wfpo "md4" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=4}) tax)
val md5 = WFCPOG_Registry.rename_wfpo "md5" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=5}) tax)
val md6 = WFCPOG_Registry.rename_wfpo "md6" (WFCPOG_Registry.TAX_Data.put ({key=9,max_depth=6}) tax)
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 wfcs = [inf,vis,md0,md1,md2,md3,md4,md5,md6,md7,md8]
val pos = [lsk,cm,sm,om,cmd,quy]
(*
val wfcs = [vis]
val pos = []
*)
fun add_dot 1 = ["."]
| add_dot x = (".")::(add_dot (x-1))
fun insert_dots string = String.concat (add_dot (20 - String.size(string)))
fun start_wfc_tests model [] = []
| start_wfc_tests model (h::wfcs) =
(case check_wfc model h of
false => ((id_of h ^ (insert_dots (id_of h)) ^ "[FAILED]\n"))::(start_wfc_tests model wfcs)
| true => ((id_of h ^ (insert_dots (id_of h)) ^ "[OK]\n"))::(start_wfc_tests model wfcs)
) handle x =>((id_of h ^ (insert_dots (id_of h)) ^ "[EXCP]\n"))::(start_wfc_tests model wfcs)
fun start_pog_tests model [] = []
| start_pog_tests model (h::wfcs) =
(case generate_po model h of
(wfc,list) => ((id_of h ^ (insert_dots (id_of h)) ^ "[ " ^ (Int.toString(List.length(list))) ^ " Terms ]\n"))::(start_wfc_tests model wfcs)
) handle x =>((id_of h ^ (insert_dots (id_of h)) ^ "[EXCP]\n"))::(start_wfc_tests model wfcs)
val buffer = ref []:string list ref
val _ = buffer := (!buffer)@["\n\n\n\n"]
(** MODELS **)
(*
val zargo = "../../../examples/SimpleChair/SimpleChair.zargo"
val ocl = "../../../examples/SimpleChair/ConcreteSimpleChair01.ocl"
val simple = import zargo ocl []
val zargo = "../../../examples/ebank/ebank.zargo"
val ocl = "../../../examples/ebank/ebank.ocl"
val ebank = import zargo ocl []
*)
(** STACK_MANU **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["STACK_MANU (without Refinement)..........[OK]\n\n"]
val zargo = "../../../examples/stack_manu/stack.zargo"
val ocl = "../../../examples/stack_manu/stack.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nSTACK_MANU finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** STACK **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["STACK (without Refinement)..........[FIXME] \n\n"]
val zargo = "../../../examples/stack/stack.zargo"
val ocl = "../../../examples/stack/stack.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nSTACK finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** EBANK **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["EBANK (without Refinement) \n\n"]
val zargo = "../../../examples/ebank/ebank.zargo"
val ocl = "../../../examples/ebank/ebank.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nEBANK finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** DIGRAPH **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["DIGRAPH (without Refinement) \n\n"]
val zargo = "../../../examples/digraph/digraph.zargo"
val ocl = "../../../examples/digraph/digraph.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nDIGRAPH finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** VEHICLES **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["VEHICLES (without Refinement) \n\n"]
val zargo = "../../../examples/vehicles/vehicles.zargo"
val ocl = "../../../examples/vehicles/vehicles.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nVEHICLES finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** ROYALS_AND_LOYALS **)
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["ROYALS_AND_LOYALS (without Refinement) \n\n"]
val zargo = "../../../examples/royals_and_loyals/royals_and_loyals.zargo"
val ocl = "../../../examples/royals_and_loyals/royals_and_loyals.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nROYALS_AND_LOYALS finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
(** CALENDAR **)
(*
val _ = buffer := (!buffer)@["***********************************\n\n"]
val _ = buffer := (!buffer)@["CALENDAR (without Refinement) \n\n"]
val zargo = "../../../examples/calendar/calendar.zargo"
val ocl = "../../../examples/calendar/calendar.ocl"
val i_model = ModelImport.import zargo ocl []
val (clist,alist) = Rep_Core.normalize_ext i_model
val model = ((clist@oclLib),(alist))
val _ = buffer := (!buffer)@[(String.concat (start_wfc_tests model wfcs))]
val _ = buffer := (!buffer)@[(String.concat (start_pog_tests model pos))]
val _ = buffer := (!buffer)@[("\nCALENDAR finished ...\n\n\n")]
val _ = buffer := (!buffer)@["***********************************\n\n\n"]
*)
val output = String.concat (!buffer)
(*
val model = []
*)

201
su4sml/src/wfcpo-gen/visibility_consistency.sml Normal file
View File

@ -0,0 +1,201 @@
(*****************************************************************************
* 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 VISIBILITY_CONSTRAINT =
sig
val are_conditions_visible : WFCPOG.wfpo -> Rep.Model -> bool
end
structure Visibility_Constraint:VISIBILITY_CONSTRAINT =
struct
(* su4sml *)
open Rep_Core
open Rep_OclTerm
open Rep_OclType
open Rep2String
open XMI_DataTypes
(* oclparser *)
open Ext_Library
open ModelImport
(* wfcpo-gen *)
open WFCPOG_Library
open WFCPO_Naming
exception WFCPO_VisibilityError of string
fun modificator_conforms_to private private = true
| modificator_conforms_to protected private = true
| modificator_conforms_to package private = true
| modificator_conforms_to public private = true
| modificator_conforms_to protected protected = true
| modificator_conforms_to package protected = true
| modificator_conforms_to public protected = true
| modificator_conforms_to package package = true
| modificator_conforms_to public package = true
| modificator_conforms_to public public = true
| modificator_conforms_to x y = false
fun is_modificator_conformant_CollPart modif (CollectionItem(term,typ)) model = is_modificator_conformant modif term model
| is_modificator_conformant_CollPart modif (CollectionRange(first,last,typ)) model =
(is_modificator_conformant modif first model) andalso (is_modificator_conformant modif last model)
and is_modificator_conformant modif (Literal(s,typ)) model = true
| is_modificator_conformant modif (Variable(s,typ)) model = true
| is_modificator_conformant modif (CollectionLiteral(part,typ)) model =
List.all (fn a => is_modificator_conformant_CollPart modif a model) part
| is_modificator_conformant modif (If(cond,cond_typ,else_t,else_typ,then_t,then_typ,rtyp)) model =
is_modificator_conformant modif cond model
andalso is_modificator_conformant modif else_t model
andalso is_modificator_conformant modif then_t model
| is_modificator_conformant modif (AssociationEndCall(src,styp,path,rtyp)) model =
let
val cl = get_classifier src model
val att_name = List.last(path)
val att = get_attribute att_name cl model
val _ = trace 100 ("end is_modificator_conformant")
in
if (modificator_conforms_to (#visibility att) modif)
then (is_modificator_conformant modif src model)
else false
end
| is_modificator_conformant modif (x as OperationCall(src,styp,path,args,rtyp)) model =
let
val typ = type_of_term src
val cl = get_classifier (Variable("x",typ)) model
val op_name = List.last(path)
val _ = trace 100 ("OperationCall: " ^ (Ocl2String.ocl2string false x) ^ "\n")
val _ = trace 100 ("Classifier : " ^ Rep2String.classifier2string cl ^ "\n")
val _ = trace 100 ("Op_name : " ^ op_name ^ "\n")
val oper = get_operation op_name cl model
val _ = trace 100 ("end is_modificator_conformant")
in
if (modificator_conforms_to (#visibility oper) modif)
then ((List.all (fn (a,b) => (is_modificator_conformant modif a model)) args) andalso (is_modificator_conformant modif src model))
else false
end
| is_modificator_conformant modif (x as AttributeCall(src,styp,path,rtyp)) model =
let
val cl = get_classifier src model
val att_name = List.last(path)
val att = get_attribute att_name cl model
val _ = trace 100 ("end is_modificator_conformant")
in
if (modificator_conforms_to (#visibility att) modif)
then (is_modificator_conformant modif src model)
else false
end
| is_modificator_conformant modif (OperationWithType(src,styp,name,ntyp,rtyp)) model = is_modificator_conformant modif src model
| is_modificator_conformant modif (Let(var,vtyp,rhs,rtyp,t_in,ityp)) model =
(is_modificator_conformant modif rhs model) andalso (is_modificator_conformant modif t_in model)
| is_modificator_conformant modif (Iterate(iter_vars,rname,rtyp,rterm,src,styp,body,btyp,retyp)) model =
(is_modificator_conformant modif src model) andalso (is_modificator_conformant modif body model)
| is_modificator_conformant modif (Iterator(name,vars,src,styp,body,btyp,rtyp)) model =
(is_modificator_conformant modif src model) andalso (is_modificator_conformant modif body model)
fun are_conditions_visible_help [] model = true
| are_conditions_visible_help (h::classes) (model as (clist,alist)) =
if (not (is_visible_cl h))
then
let
val _ = trace 50 ("Classifier " ^ (string_of_path (name_of h)) ^ " is not visible.\n")
in
are_conditions_visible_help classes model
end
else
let
val _ = trace 50 ("Classifier " ^ (string_of_path (name_of h)) ^ " is visible.\n")
val pub_op = List.map (fn a =>
let
val _ = trace 100 ("public operation = " ^ (name_of_op a) ^ "\n")
val posts = postcondition_of_op a
in
List.map (fn (x,y) => is_modificator_conformant public y model) posts
end
) (public_operations_of (name_of h) model)
val _ = trace 50 ("public operations done.\n\n")
val pac_op = List.map (fn a =>
let
val _ = trace 100 ("package operations ...\n")
val posts = postcondition_of_op a
in
List.map (fn (x,y) => is_modificator_conformant package y model) posts
end
) (package_operations_of (name_of h) model)
val _ = trace 50 ("package operations done.\n\n")
val pro_op = List.map (fn a =>
let
val _ = trace 100 ("protected operations ...\n")
val posts = postcondition_of_op a
in
List.map (fn (x,y) => is_modificator_conformant protected y model) posts
end
) (protected_operations_of (name_of h) model)
val _ = trace 50 ("protected operations done.\n\n")
val _ = trace 50 ("visibility" ^ (string_of_path (name_of h)) ^ " done.\n")
in
if (List.all (fn a => a) (List.concat (pub_op@pro_op@pac_op)))
then are_conditions_visible_help classes model
else false
end
fun are_conditions_visible wfpo (model:Rep.Model as (clist,alist)) =
let
val _ = trace 50 ("Visibility Constraint starts ...\n")
val classes = removeOclLibrary clist
val _ = trace 50 ("OclLibrary removed ...\n")
in
are_conditions_visible_help classes model
end
end;

20
su4sml/src/wfcpo-gen/wfcpo.cm
View File

@ -51,16 +51,20 @@ Group is
$smlnj/basis/basis.cm
$smlnj/ml-yacc/ml-yacc-lib.cm
#endif
"datatab.sml"
"wfcpog.sml"
"wfcpog_registry.sml"
"naming.sml"
"constraint.sml"
"base_constraint.sml"
"plugin_constraint.sml"
"library.sml"
"liskov_constraint.sml"
"liskov_constraint.sml"
"data_model_consistency.sml"
"constructor_consistency.sml"
(* "operational_consistency.sml" *)
"refine_constraint.sml"
"registry.sml"
"operational_consistency.sml"
"refine_constraint.sml"
"command_query_consistency.sml"
"visibility_consistency.sml"
"taxonomy_consistency.sml"
"interface_consistency.sml"
"wfcpog_constraint_library.sml"

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

@ -1,26 +0,0 @@
(* 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
*)

217
su4sml/src/wfcpo-gen/wfcpog.sml Normal file
View File

@ -0,0 +1,217 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* wfcpog.sml ---
* This file is part of su4sml.
*
* Copyright (c) 2008 Achim D. Brucker, Germany
*
* 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: wfcpog.sml 7273 2008-02-18 07:18:05Z brucker $ *)
signature WFCPOG =
sig
type wfpo_id = string
datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool
| POG of wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
and
wfpo = WFPO of {
identifier : wfpo_id, (* identifier *)
name : string, (* short description (for output) *)
description : string, (* long description *)
recommended : bool, (* presented to the end-user? *)
depends : wfpo_id list, (* wfcpos that must be applied *)
recommends : wfpo_id list, (* wfcpos that should be applied *)
apply : wf_or_po, (* apply this wf check or po gen. *)
data : Object.T Datatab.table (* arbitrary data, mainly used
for configuration data *)
}
val get_data : wfpo -> Object.T Datatab.table
val up_data : Object.T Datatab.table -> wfpo -> wfpo
val is_wfc : wfpo -> bool
val is_pog : wfpo -> bool
val apply_of : wfpo -> wf_or_po
val id_of : wfpo -> wfpo_id
end
structure WFCPOG:WFCPOG =
struct
type wfpo_id = string
datatype wf_or_po = WFC of wfpo -> Rep.Model -> bool
| POG of wfpo -> Rep.Model -> Rep_OclTerm.OclTerm list
and wfpo = WFPO of {
identifier : wfpo_id, (* identifier *)
name : string, (* short description (for output) *)
description : string, (* long description *)
recommended : bool, (* presented to the end-user? *)
depends : wfpo_id list,
recommends : wfpo_id list,
apply : wf_or_po,
data : Object.T Datatab.table
}
fun get_data (WFPO w) = #data w
fun up_data data' (WFPO{identifier=identifier,name=name,description=description,
recommended=recommended, depends=depends,recommends=remommends,apply=apply,
data=data})
= (WFPO{identifier=identifier,name=name,description=description,
recommended=recommended, depends=depends,recommends=remommends,apply=apply,
data=data'})
fun is_wfc (WFPO {apply=apply,...}) = (case apply of
WFC _ => true
| _ => false )
fun is_pog (WFPO {apply=apply,...}) = (case apply of
POG _ => true
| _ => false )
fun apply_of (WFPO {apply=apply,...}) = apply
fun id_of (WFPO{identifier=identifier,...}) = identifier
end
signature WFPO_DATA_ARGS =
sig
type T
val empty: T
val copy: T -> T
val extend: T -> T
end;
signature WFPO_DATA =
sig
type T
val get: WFCPOG.wfpo -> T
val put: T -> WFCPOG.wfpo -> WFCPOG.wfpo
val map: (T -> T) -> WFCPOG.wfpo -> WFCPOG.wfpo
end;
signature PRIVATE_WFPO_DATA =
sig
type serial
exception error of string
val declare : Object.T
-> (Object.T -> Object.T) -> (Object.T -> Object.T) -> serial
val get : serial -> (Object.T -> 'a) -> WFCPOG.wfpo -> 'a
val put : serial -> ('a -> Object.T) -> 'a -> WFCPOG.wfpo -> WFCPOG.wfpo
end
structure WfpoData:PRIVATE_WFPO_DATA =
struct
exception error of string
type kind =
{empty: Object.T,
copy: Object.T -> Object.T,
extend: Object.T -> Object.T
};
val kinds = ref (Datatab.empty: kind Datatab.table)
fun invoke f k =
(case Datatab.lookup (! kinds) k of
SOME kind => f kind
| NONE => raise error "Invalid wfpo data identifier");
fun invoke_empty k = invoke ((fn x => fn _ => x) o #empty) k ();
val invoke_copy = invoke #copy;
val invoke_extend = invoke #extend;
type serial = int;
local
val count = ref (0: int)
fun inc i = (i := ! i + (1: int); ! i);
in
fun serial () = inc count
end
fun change r f = r := f (! r);
fun declare empty copy extend =
let
fun CRITICAL a = a ()
val k = serial ();
val kind = {empty = empty, copy = copy, extend = extend};
val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
in k end;
fun get k dest wfpo =
dest ((case Datatab.lookup (WFCPOG.get_data wfpo) k of
SOME x => x
| NONE => invoke_copy k (invoke_empty k) )) (*adhoc value*)
fun put k mk x =
let
fun modify_wfpo f x = WFCPOG.up_data (f (WFCPOG.get_data x)) x
in
modify_wfpo (Datatab.update (k, mk x))
end
end;
functor WfpoDataFun(Data: WFPO_DATA_ARGS) : WFPO_DATA =
struct
structure WfpoData = WfpoData;
type T = Data.T;
exception Data of T;
val kind = WfpoData.declare
(Data Data.empty)
(fn Data x => Data (Data.copy x))
(fn Data x => Data (Data.extend x))
;
val get = WfpoData.get kind (fn Data x => x);
val put = WfpoData.put kind Data;
fun map f wfpo = put (f (get wfpo)) wfpo;
end;

7
su4sml/src/wfcpo-gen/wfcpog_constraint_library.sml Normal file
View File

@ -0,0 +1,7 @@
structure WFCPOG_Constraint_Library =
struct
open WFCPOG_Registry
open WFCPOG
end;

297
su4sml/src/wfcpo-gen/wfcpog_registry.sml Normal file
View File

@ -0,0 +1,297 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* ---
* This file is part of su4sml.
*
* Copyright (c) 2008 Achim D. Brucker, Germany
*
* 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: wfcpog_registry.sml 7273 2008-02-18 07:18:05Z brucker $ *)
signature WFCPOG_REGISTRY =
sig
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
val add_wfpo : WFCPOG.wfpo -> unit
val del_wfpo : WFCPOG.wfpo_id -> unit
val rename_wfpo : string -> WFCPOG.wfpo -> WFCPOG.wfpo
val get_wfpo : WFCPOG.wfpo list -> WFCPOG.wfpo_id -> WFCPOG.wfpo
val check_wfc : Rep.Model -> WFCPOG.wfpo -> bool
val check_wfcs : Rep.Model -> WFCPOG.wfpo list -> bool
val generate_po : Rep.Model -> WFCPOG.wfpo -> (WFCPOG.wfpo * Rep_OclTerm.OclTerm list)
val generate_pos : Rep.Model -> WFCPOG.wfpo list -> (WFCPOG.wfpo * Rep_OclTerm.OclTerm list) list
exception WFCPOG_RegistryError of string
end
structure WFCPOG_Registry :WFCPOG_REGISTRY =
struct
exception WFCPOG_RegistryError of string
structure LSK_Data = Liskov_Constraint.LSK_Data
structure TAX_Data = Taxonomy_Constraint.TAX_Data
structure RFM_Data = Refine_Constraint.RFM_Data
open Ext_Library
open WFCPOG
val wfpos = ref ([]:(WFCPOG.wfpo list))
fun wfcpog_of id = hd (List.filter (fn m => WFCPOG.id_of m = id) (!wfpos))
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")
| get_wfpo (h::tail) x =
if (id_of h = x)
then h
else get_wfpo tail x
fun rename_wfpo new_name (WFCPOG.WFPO{identifier=identifier,name=name,description=description,recommended=recommended,depends=depends,recommends=recommends,apply=apply,data=data}:WFCPOG.wfpo) =
WFCPOG.WFPO{
identifier=new_name,
name=name,
description=description,
recommended=recommended,
depends=depends,
recommends=recommends,
apply=apply,
data=data
}
fun check_wfc model (wfc_sel) =
let
val _ = trace 10 (id_of wfc_sel ^ "..............")
val apply = case WFCPOG.apply_of wfc_sel of
(WFCPOG.WFC a ) => a wfc_sel
| _ => (fn _ => true)
val res = apply (model)
val _ = case res of
false => trace 10 ("[FAILED]\n")
| true => trace 10 ("[OK]\n")
in
res
end
fun check_wfcs model wfcs = List.all (fn v => (v = true))
(map (check_wfc model) wfcs)
fun generate_po model (wfc_sel) =
let
val apply = case WFCPOG.apply_of wfc_sel of
(WFCPOG.POG a) => a wfc_sel
| _ => (fn _ => [])
in
(wfc_sel, (apply (model)) )
end
fun generate_pos model wfcs = map (generate_po model) wfcs
val supported = [
WFCPOG.WFPO{
identifier = "lsk_pre",
name = "Liskov weaken_precondition",
description = "Generate Proof Obligations for weaking precondition",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Liskov_Constraint.weaken_precondition),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "lsk_post",
name = "Liskov strengthen_postcondition", (* short description (for output) *)
description = "Generate Proof Obligations following from strengthen_postcondition",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Liskov_Constraint.strengthen_postcondition),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "lsk_inv",
name = "Liskov conjugate_invariants",
description = "Generate Proof Obligations following from conjugate_invariants",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Liskov_Constraint.conjugate_invariants),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "lsk",
name = "Liskov's subtitution principle",
description = "Generate Proof Obligations following the idea from Barbara Liskov",
recommended = true,
depends = ["lsk_pre","lsk_post"],
recommends = [],
apply = WFCPOG.POG(Liskov_Constraint.conjugate_invariants),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "inf_ster",
name = "Interfas has_consistent_stereotypes",
description = "Checks if all operations of an interface do not have stereotypes create or destroy.",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.WFC(Interface_Constraint.has_consistent_stereotypes),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "inf_name",
name = "Interface is_nameclash_free",
description = "Checks for classes inheriting from more than one interface that there are no nameclashes.",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.WFC(Interface_Constraint.is_nameclash_free),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "inf",
name = "Interface complete",
description = "Checks has_consistent_stereotypes and is_nameclash_free",
recommended = true,
depends = ["inf_ster"],
recommends = [],
apply = WFCPOG.WFC(Interface_Constraint.is_nameclash_free),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "class_model", (* identifier *)
name = "Data model consistency",
description = "Data model consistency; a classes should be able to be instantiated from a state.",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Data_Model_Consistency_Constraint.class_model_consistency),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "strong_model", (* identifier *)
name = "Data model consistency",
description = "Data model consistency; all classes should be able to be instantiated from a state.",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Data_Model_Consistency_Constraint.strong_model_consistency),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "oper_model", (* identifier *)
name = "Operational model consistency",
description = "Inserts the additional proof obligations resulting from the SecureUML transformation",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Operational_Constraint.generate_pos),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "cmd", (* identifier *)
name = "Query Command Constraint",
description = "Check if operations which are declared as command are really commands",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Command_Query_Constraint.ops_are_command),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "quy", (* identifier *)
name = "Query Command Constraint",
description = "Check if operations which are declared as queries are really queries",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.POG(Command_Query_Constraint.ops_are_query),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "vis", (* identifier *)
name = "Visibility Constraint",
description = "Check if the accessed operations in preconditions/postconditions/invariants are visible.",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.WFC(Visibility_Constraint.are_conditions_visible),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "tax", (* identifier *)
name = "Max Depth",
description = "Max Depth",
recommended = true,
depends = [],
recommends = [],
apply = WFCPOG.WFC(Taxonomy_Constraint.has_maxDepth),
data = Datatab.empty
},
WFCPOG.WFPO{
identifier = "rfm_syn",
name = "OO Refinement",
description = "Check if public classes of aboriginal are also public in new Package",
recommended = false,
depends = [],
recommends = [],
apply = WFCPOG.WFC(Refine_Constraint.check_syntax),
data = Datatab.empty
},
WFCPOG.WFPO {
identifier = "ref_po",
name = "OO Refinement",
description = "Generate Proof Obligations for OO data refinement",
recommended = true,
depends = [],
recommends = [],
apply = WFCPOG.POG(Refine_Constraint.refine_po),
data = Datatab.empty
}]
end