223 lines
8.0 KiB
Standard ML
223 lines
8.0 KiB
Standard ML
(*****************************************************************************
|
|
* 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
|
|
* 2008-2009 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: context_declarations.sml 6727 2007-07-30 08:43:40Z brucker $ *)
|
|
|
|
(** Implementation of the Liskov Substitiution Principle. *)
|
|
signature WFCPOG_LISKOV_CONSTRAINT =
|
|
sig
|
|
type Liskov_args
|
|
|
|
structure WFCPOG_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_OclType.Path * Rep_OclTerm.OclTerm) list
|
|
|
|
(** sub constraint, included in liskov.*)
|
|
val strengthen_postcondition : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
|
|
|
|
(** sub constraint, included in liskov.*)
|
|
val conjugate_invariants : WFCPOG.wfpo -> Rep.Model -> (Rep_OclType.Path * Rep_OclTerm.OclTerm) list
|
|
|
|
end
|
|
structure WFCPOG_Liskov_Constraint : WFCPOG_LISKOV_CONSTRAINT =
|
|
struct
|
|
|
|
exception WFCPOG_LiskovError of string
|
|
(* su4sml *)
|
|
open Rep_Core
|
|
open Rep_OclTerm
|
|
open Rep_OclType
|
|
open Rep2String
|
|
open Rep_HolOcl_Namespace
|
|
(* oclparser *)
|
|
open ModelImport
|
|
|
|
(* wfcpo-gen *)
|
|
open WFCPOG_Library
|
|
open Datatab
|
|
exception WFCPO_LiskovError of string
|
|
|
|
type Liskov_args = {
|
|
model:string,
|
|
size:int
|
|
}
|
|
|
|
|
|
datatype lisk_type = weaken_pre | strengthen_post
|
|
|
|
structure WFCPOG_LSK_Data = WFCPOG_DataFun
|
|
(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 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
|
|
val super_type = Rep_Core.type_of super_class
|
|
val sub_type = Rep_Core.type_of sub_class
|
|
fun OclLocalValid t = (OperationCall (t,
|
|
Boolean,["holOclLib","Boolean","OclLocalValid"],
|
|
[(Literal("\\<tau>",OclState),DummyT)],Boolean))
|
|
in
|
|
case typ of
|
|
weaken_pre =>
|
|
(* DEFINITION (OOSC p.578): super_pre -> sub_pre*)
|
|
let
|
|
val pre_super = Predicate(Variable("self_super",super_type),super_type,
|
|
name_of_pre super_class oper,
|
|
args2varargs (arguments_of_op op_of_super))
|
|
val pre_sub = Predicate(Variable("self_sub", sub_type),sub_type,
|
|
name_of_pre sub_class oper,
|
|
args2varargs (arguments_of_op op_of_super))
|
|
|
|
in
|
|
OperationCall(OclLocalValid pre_super,Boolean,["holOclLib","Boolean","implies"],
|
|
[(OclLocalValid pre_sub,Boolean)],Boolean)
|
|
end
|
|
| strengthen_post =>
|
|
(* DEFINITION (OOSC p.578): sub_posts -> super_post *)
|
|
let
|
|
val post_super = Predicate(Variable("self_super",Rep_Core.type_of super_class),
|
|
Rep_Core.type_of super_class,
|
|
name_of_post super_class oper,
|
|
args2varargs ((arguments_of_op op_of_super)@[("result",DummyT)]))
|
|
val post_sub = Predicate(Variable("self_sub",Rep_Core.type_of sub_class),
|
|
Rep_Core.type_of sub_class,
|
|
name_of_post sub_class oper,
|
|
args2varargs ((arguments_of_op op_of_super)@[("result",DummyT)]))
|
|
in
|
|
OperationCall(OclLocalValid post_sub,Boolean,["holOclLib","Boolean","implies"],
|
|
[(OclLocalValid post_super,Boolean)],Boolean)
|
|
end
|
|
end
|
|
|
|
|
|
fun weaken_precondition_help [] model = []
|
|
| weaken_precondition_help (class::clist) model =
|
|
let
|
|
val mo = modified_operations_of class model
|
|
(* (operation of subclass, classifier of super class) *)
|
|
val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo
|
|
(* proofs obligation for classifier [(term,constraint info)] *)
|
|
val pos = List.map (fn (a,b) => (["po_lsk_pre_"]@(name_of class)@["_"]@[name_of_op a],
|
|
generate_return_value weaken_pre a class b model)) raw_po
|
|
in
|
|
pos@(weaken_precondition_help clist model)
|
|
end
|
|
|
|
fun weaken_precondition wfpo (model as (clist,alist)) =
|
|
let
|
|
val cl = removeOclLibrary clist
|
|
in
|
|
weaken_precondition_help cl model
|
|
end
|
|
|
|
|
|
fun strengthen_postcondition_help [] model = []
|
|
| strengthen_postcondition_help (class::clist) model =
|
|
let
|
|
val mo = modified_operations_of class model
|
|
(* (operation of subclass, classifier of super class) *)
|
|
val raw_po = List.map (fn a => (a,(go_up_hierarchy class (class_contains_op a model) model))) mo
|
|
(* proof obligations for classifier [(term,constraint info)] *)
|
|
val pos = List.map (fn (a,b) => (["po_lsk_post"]@["_"]@(name_of class)@["_"]@[name_of_op a],
|
|
generate_return_value strengthen_post a class b model)) raw_po
|
|
in
|
|
pos@(strengthen_postcondition_help clist model)
|
|
end
|
|
|
|
fun strengthen_postcondition wfpo (model as (clist,alist)) =
|
|
let
|
|
val cl = removeOclLibrary clist
|
|
in
|
|
strengthen_postcondition_help cl model
|
|
end
|
|
|
|
|
|
|
|
|
|
fun conjugate_invariants_help [] model = []
|
|
| conjugate_invariants_help (class::clist) model =
|
|
let
|
|
(* get the invariants of all parents *)
|
|
val parents_and_self = (parents_of class model)@[class]
|
|
val invs = List.map (fn a =>
|
|
let
|
|
val term = Predicate(Variable(varcounter.nextStr(),Rep_Core.type_of a),Rep_Core.type_of a,name_of_inv a,[])
|
|
in
|
|
Rep_HolOcl_Helper.holocl_localValid_state term "\\<tau>"
|
|
end) parents_and_self
|
|
in
|
|
if (List.length(invs) = 0)
|
|
then (conjugate_invariants_help clist model)
|
|
else (["po_lsk_inv"]@["_"]@(name_of class)@["_"],
|
|
Rep_HolOcl_Helper.holocl_and_all invs)::(conjugate_invariants_help clist model)
|
|
|
|
end
|
|
|
|
fun conjugate_invariants wfpo (model as (clist,alist)) =
|
|
let
|
|
val cl = removeOclLibrary clist
|
|
in
|
|
conjugate_invariants_help cl model
|
|
end
|
|
|
|
end
|