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

added USE-Cartridge (beta version) 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@6694 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Achim D. Brucker 2007-07-16 06:05:43 +00:00
parent 5f52c9b43a
commit 77a74ca594
9 changed files with 443 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/codegen/ROOT.ML
View File

@ -61,6 +61,7 @@ use "componentuml_cartridge.sml";
use "java_cartridge.sml";
use "junit_cartridge.sml";
use "maven_pom_cartridge.sml";
use "use_cartridge.sml";
(* Statemachines *)

107
src/codegen/base_cartridge.sml
View File

@ -40,7 +40,7 @@
(* $Id$ *)
(**
* This cartridge knows about the basic elements of UML class diagrams.
* This cartridge knows about the basic elements of UML class models.
* The elements are classifiers, attributes, and operations with their
* parameters in terms of the Rep interface
*)
@ -90,8 +90,11 @@ type Model = Rep.Classifier list
type environment = { model : Model,
counter : int ref,
curClassifier: Rep_Core.Classifier option,
curInvariant : (string option * Rep_OclTerm.OclTerm) option,
curAssocEnd : Rep_Core.associationend option,
curOperation : Rep_Core.operation option,
curPrecondition : (string option * Rep_OclTerm.OclTerm) option,
curPostcondition: (string option * Rep_OclTerm.OclTerm) option,
curAttribute : Rep_Core.attribute option ,
curArgument : (string * Rep_OclType.OclType) option
}
@ -108,6 +111,9 @@ fun curArgument (env : environment) = (#curArgument env)
fun curClassifier' (env : environment) = Option.valOf((#curClassifier env))
fun curAttribute' (env : environment) = Option.valOf((#curAttribute env))
fun curInvariant' (env : environment) = Option.valOf((#curInvariant env))
fun curPrecondition' (env : environment) = Option.valOf((#curPrecondition env))
fun curPostcondition' (env : environment) = Option.valOf((#curPostcondition env))
fun curAssociationEnd' (env : environment) = Option.valOf((#curAssocEnd env))
fun curOperation' (env : environment) = Option.valOf((#curOperation env))
fun curArgument' (env : environment) = Option.valOf((#curArgument env))
@ -115,8 +121,11 @@ fun curArgument' (env : environment) = Option.valOf((#curArgument env))
fun initEnv model = { model = model,
counter = ref 0,
curClassifier = NONE,
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE } : environment
@ -142,8 +151,22 @@ fun lookup env "classifier_name" = Rep_Core.short_name_of (curClassifier' env
| lookup env "classifier_package_path" = curClassifierPackageToString env Rep_OclType.pathstring_of_path
| lookup env "classifier_parent" = Rep_Core.short_parent_name_of (curClassifier' env)
| lookup env "attribute_name" = #name (curAttribute' env)
| lookup env "attribute_type" = oclType2Native (#attr_type
(curAttribute' env))
| lookup env "attribute_type" = oclType2Native (#attr_type (curAttribute' env))
| lookup env "inv_name" = (case #1 (curInvariant' env) of
NONE => ""
| SOME n => n )
| lookup env "inv_cs" = (Ocl2String.ocl2string false) (#2 (curInvariant' env))
| lookup env "post_name" = (case #1 (curPostcondition' env) of
NONE => ""
| SOME n => n )
| lookup env "post_cs" = (Ocl2String.ocl2string false) (#2 (curPostcondition' env))
| lookup env "pre_name" = (case #1 (curPrecondition' env) of
NONE => ""
| SOME n => n )
| lookup env "pre_cs" = (Ocl2String.ocl2string false) (#2 (curPrecondition' env))
| lookup env "attribute_visibility" = visibility2Native(#visibility
(curAttribute' env))
| lookup env "attribute_scope" = scope2Native (#scope (curAttribute' env))
@ -195,6 +218,10 @@ fun test env "isClass" = (case (#curClassifier env) of
(parentName <> "oclLib.OclAny")
end
| test env "hasOperations" = (length (Rep_Core.operations_of (curClassifier' env))) > 0
| test env "hasInvariants" = (length (Rep_Core.invariant_of (curClassifier' env))) > 0
| test env "hasOpSpec" = ((length (Rep_Core.precondition_of_op (curOperation' env)))
+(length (Rep_Core.postcondition_of_op (curOperation' env)))) > 0
| test env "hasAttributes" = (length (Rep_Core.attributes_of (curClassifier' env))) > 0
| test env "first_classifier" = (curClassifier' env = hd (#model env))
| test env "first_attribute" = (curAttribute' env
= hd (Rep_Core.attributes_of (curClassifier' env)))
@ -232,8 +259,11 @@ fun foreach_classifier (env : environment)
fun env_from_classifier c = { model = #model env,
counter = #counter env,
curClassifier= SOME c,
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE }
in
@ -249,21 +279,80 @@ fun foreach_nonprimitive_classifier (env : environment)
fun env_from_classifier c = { model = (#model env),
counter = #counter env,
curClassifier = SOME c,
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE }
in
List.map env_from_classifier cl
end
fun foreach_invariant (env : environment)
= let val invs = Rep_Core.invariant_of (curClassifier' env)
fun env_from_inv inv = { model = (#model env),
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = SOME inv,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE }
in
List.map env_from_inv invs
end
fun foreach_precondition (env : environment)
= let val pres = Rep_Core.precondition_of_op (curOperation' env)
fun env_from_pre pre = { model = (#model env),
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = SOME pre,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE }
in
List.map env_from_pre pres
end
fun foreach_postcondition (env : environment)
= let val posts = Rep_Core.postcondition_of_op (curOperation' env)
fun env_from_post post = { model = (#model env),
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = SOME post,
curAttribute = NONE,
curArgument = NONE }
in
List.map env_from_post posts
end
fun foreach_attribute (env : environment)
= let val attrs = Rep_Core.attributes_of (curClassifier' env)
fun env_from_attr a = { model = #model env,
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curAssocEnd = NONE,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = SOME a,
curArgument = NONE }
in
@ -275,7 +364,10 @@ fun foreach_operation (env : environment)
fun env_from_op operation = { model = #model env,
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curOperation = SOME operation,
curPrecondition = NONE,
curPostcondition = NONE,
curAssocEnd = NONE,
curAttribute = NONE,
curArgument = NONE }
@ -288,7 +380,10 @@ fun foreach_argument (env : environment)
fun env_from_argument arg = { model = #model env,
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curOperation = SOME (curOperation' env),
curPrecondition = NONE,
curPostcondition = NONE,
curAssocEnd = NONE,
curAttribute = NONE,
curArgument = SOME arg }
@ -301,8 +396,11 @@ fun foreach_assocend (env : environment)
fun env_from_argument arg = { model = #model env,
counter = #counter env,
curClassifier = SOME (curClassifier' env),
curInvariant = NONE,
curAssocEnd = SOME arg,
curOperation = NONE,
curPrecondition = NONE,
curPostcondition = NONE,
curAttribute = NONE,
curArgument = NONE }
in
@ -322,6 +420,9 @@ fun foreach "classifier_list" env = foreach_classifier env
| foreach "attribute_list" env = foreach_attribute env
| foreach "operation_list" env = foreach_operation env
| foreach "argument_list" env = foreach_argument env
| foreach "invariant_list" env = foreach_invariant env
| foreach "precondition_list" env = foreach_precondition env
| foreach "postcondition_list" env = foreach_postcondition env
| foreach "nonprimitive_classifier_list" env = foreach_nonprimitive_classifier env
| foreach "assocend_list" env = foreach_assocend env
(* hier muss man das Environment noch etwas umpacken

70
src/codegen/codegen.110.62.cm Normal file
View File

@ -0,0 +1,70 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* codegen.110.62.cm ---
* This file is part of su4sml.
*
* Copyright (c) 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: codegen.cm 40127 2007-07-04 06:41:30Z brucker $ *)
Group is
#if(defined(NEW_CM))
$smlnj/basis/basis.cm
$smlnj/compiler/compiler.cm
$smlnj/smlnj-lib/smlnj-lib.cm
../su4sml.110.62.cm
#else
#endif
cartridge.sig
security_cartridge.sig
gcg_helper.sml
tpl_parser.sml
SM_helper.sml
stateMachine.sml
stateMachineTypes.sml
base_cartridge.sml
stringHandling.sml
c#_cartridge.sml
c#_net1_cartridge.sml
secureuml_cartridge.sml
design_cartridge.sig
componentuml_cartridge.sml
c#sm_cartridge.sml
java_cartridge.sml
junit_cartridge.sml
maven_pom_cartridge.sml
use_cartridge.sml
gcg_core.sml
codegen.sml

1
src/codegen/codegen.cm
View File

@ -65,5 +65,6 @@ Group is
java_cartridge.sml
junit_cartridge.sml
maven_pom_cartridge.sml
use_cartridge.sml
gcg_core.sml
codegen.sml

1
src/codegen/codegen.mlb
View File

@ -65,6 +65,7 @@ in
java_cartridge.sml
junit_cartridge.sml
maven_pom_cartridge.sml
use_cartridge.sml
secureuml_cartridge.sig
secureuml_cartridge.sml
design_cartridge.sig

10
src/codegen/codegen.sml
View File

@ -70,6 +70,8 @@ structure Junit_Gcg = GCG_Core (Junit_Cartridge(Java_Cartridge(Base_Cartridge)))
structure Java_Ocl_Gcg = GCG_Core (Java_Cartridge(Base_Cartridge))
structure Use_Gcg = GCG_Core (Use_Cartridge(Base_Cartridge))
structure SecureMova_Gcg = GCG_Core (ComponentUML_Cartridge(Base_Cartridge))
structure Maven_POM_Gcg = GCG_Core (Maven_POM_Cartridge(Base_Cartridge))
@ -162,6 +164,14 @@ val supported_cartridges = [
generator = Java_Ocl_Gcg.generate,
parser = RepParser.readFile,
template = "java_ocl.tpl"},
(* USE (UML Specification Environment) Cartridge *)
{lang = "USE",
name = "USE Cartridge",
description = "",
recommended = true,
generator = Use_Gcg.generate,
parser = RepParser.readFile,
template = "use.tpl"},
(* SecureMOVA Cartridge *)
{lang = "securemova",
name = "SecureMOVA Cartridge",

142
src/codegen/templates/use.tpl Normal file
View File

@ -0,0 +1,142 @@
@//////////////////////////////////////////////////////////////////////////////
@// su4sml --- a SML repository for managing (Secure)UML/OCL models
@// http://projects.brucker.ch/su4sml/
@//
@// use.tpl --- Template for USE (UML Specification Environment)
@// This file is part of su4sml.
@//
@// Copyright (c) 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: use.tpl 40127 2007-07-04 06:41:30Z brucker $
@openfile $classifier_package$.use
@nl
@nl model $classifier_package$
@foreach nonprimitive_classifier_list
@nl
@nl
@if isClass
class $classifier_name$
@end
@if isInterface
interface $classifier_name$
@end
@if isEnumeration
enum $classifier_name$ {
@end
@if notInterface
@if hasParent
< $classifier_parent$
@end
@end
@nl
@if notInterface
@if hasAttributes
@spc@spc@spc@spc attributes
@foreach attribute_list
@nl@tab$attribute_name$ : $attribute_type$
@end
@nl
@end
@end
@nl
@if hasOperations
@spc@spc@spc@spc operations
@foreach operation_list
@nl @tab@tab $operation_name$(
@foreach argument_list
@if last_argument
$argument_name$ : $argument_type$
@else
$argument_name$ : $argument_type$,
@end
@end
) : $operation_result_type$
@end
@end
@nl
@if isClass
end
@end
@if isEnumeration
}
@end
@end
@nl
@nl
constraints@nl
@foreach nonprimitive_classifier_list
@if hasInvariants
context $classifier_name$ @nl
@foreach invariant_list
@spc@spc inv $inv_name$: $inv_cs$ @nl
@end
@nl
@end
@if hasOperations
@foreach operation_list
@if hasOpSpec
@nl context $classifier_name$::$operation_name$(
@foreach argument_list
@if last_argument
$argument_name$ : $argument_type$
@else
$argument_name$ : $argument_type$,
@end
@end
) : $operation_result_type$
@nl
@foreach precondition_list
@spc@spc pre $pre_name$: $pre_cs$ @nl
@end
@foreach postcondition_list
@spc@spc post $post_name$: $post_cs$ @nl
@end
@end
@nl
@end
@end
@end
@end

110
src/codegen/use_cartridge.sml Normal file
View File

@ -0,0 +1,110 @@
(*****************************************************************************
* su4sml --- a SML repository for managing (Secure)UML/OCL models
* http://projects.brucker.ch/su4sml/
*
* use_cartridge.sml --- USE (UML Specification Environment) cartridge
* This file is part of su4sml.
*
* Copyright (c) 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: USE_cartridge.sml 40127 2007-07-04 06:41:30Z brucker $ *)
functor Use_Cartridge(SuperCart : BASE_CARTRIDGE) : BASE_CARTRIDGE =
struct
type Model = SuperCart.Model
type environment = { extension : SuperCart.environment }
fun initEnv model = { extension = SuperCart.initEnv model } : environment
fun unpack (env : environment) = #extension env
fun pack superEnv = {extension = superEnv} : environment
(* for BASE_CARTRIDGE *)
fun curClassifier env = SuperCart.curClassifier (unpack env)
fun curArgument env = SuperCart.curArgument (unpack env)
fun curOperation env = SuperCart.curOperation (unpack env)
fun curAttribute env = SuperCart.curAttribute (unpack env)
fun curAssociationEnd env = SuperCart.curAssociationEnd (unpack env)
fun curClassifier' env = Option.valOf(curClassifier env)
fun curOperation' env = Option.valOf(curOperation env)
open Rep_OclType
fun localString_of_OclType Integer = "Integer"
| localString_of_OclType Real = "Real"
| localString_of_OclType String = "String"
| localString_of_OclType Boolean = "Boolean"
| localString_of_OclType OclAny = "OclAny"
| localString_of_OclType (Set t) = ("Set("^(localString_of_OclType t)^")")
| localString_of_OclType (Sequence t) = ("Sequence("^(localString_of_OclType t)^")")
| localString_of_OclType (OrderedSet t) = ("OrderedSet("^(localString_of_OclType t)^")")
| localString_of_OclType (Bag t) = ("Bag("^(localString_of_OclType t)^")")
| localString_of_OclType (Collection t) = ("Collection("^(localString_of_OclType t)^")")
| localString_of_OclType OclVoid = "OclVoid"
| localString_of_OclType (Classifier p) = (hd (rev p))
| localString_of_OclType DummyT = "DummyT"
| localString_of_OclType (TemplateParameter s) = "TemplateParameter \""^s^"\""
(* any special variables? *)
fun lookup env "attribute_type" = localString_of_OclType (#attr_type (valOf (curAttribute env)))
| lookup env "argument_type" = localString_of_OclType (#2 (valOf (curArgument env)))
| lookup env "assocend_type"
= ((localString_of_OclType o #aend_type o valOf o curAssociationEnd) env)
| lookup env "operation_result_type" = localString_of_OclType (Rep.result_of_op
(valOf (curOperation env)))
| lookup (env : environment) s = SuperCart.lookup (unpack env) s
(* any special predicates?*)
fun test (env : environment) s = SuperCart.test (unpack env) s
(* any special lists? *)
fun foreach listType (env : environment) = map pack (SuperCart.foreach listType (unpack env))
end
(*
fun test () =
let
val uml = "/home/brucker/infsec/src/HOL-OCL/hol-ocl/examples/company/company.zargo"
val ocl = "/home/brucker/infsec/src/HOL-OCL/hol-ocl/examples/company/company.ocl"
val model = map Rep.normalize (ModelImport.import uml ocl [])
in
Codegen.generateFromModel model "USE"
end
*)

6
src/ocl2string.sml
View File

@ -100,8 +100,8 @@ fun ocl2string show_types oclterm =
(**************************************)
(* OCL Boolean *)
Literal (s, String) => if show_types
then "(\""^s^"\":"^(string_of_OclType String)^")"
else "\""^s^"\""
then "("^s^":"^(string_of_OclType String)^")"
else ""^s^""
| Literal (lit, typ) => if show_types
then "("^lit^":"^(string_of_OclType typ)^")"
else lit
@ -166,6 +166,8 @@ fun ocl2string show_types oclterm =
=> OclSubString u (ocl2string u src) (ocl2string u b) (ocl2string u e)
*)
| OperationCall (src,styp,["oclLib",classifier,"allInstances"],[],_)
=> (string_of_OclType (Rep_OclHelper.type_of src))^"::allInstances()"
| OperationCall (src,styp,["oclLib",classifier,opname],[],rtyp) => string_of_oo_postfix1 show_types src styp opname rtyp
| OperationCall (src,styp,["oclLib",classifier,opname],[(arg,atyp)],rtyp) => string_of_oo_infix show_types src styp opname arg atyp rtyp