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

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

This commit is contained in:
Achim D. Brucker 2008-04-02 22:10:37 +00:00
parent 0f01f3e8d1
commit 31b8e9a2ed
3 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
su4sml/src/wfcpog/ROOT.ML
View File

@ -41,7 +41,6 @@
use "holocl_namespace.sml";
use "datatab.sml";
use "naming.sml";
use "library.sml";
use "wfcpog.sml";
@ -51,12 +50,11 @@ use "liskov_constraint.sml";
use "data_model_consistency.sml";
use "constructor_consistency.sml";
use "operational_consistency.sml";
(* TODO: use "refine_constraint.sml"; *)
use "refine_constraint.sml";
use "command_query_consistency.sml";
(* TODO: use "taxonomy_consistency.sml"; *)
use "taxonomy_consistency.sml";
use "interface_consistency.sml";
(* wccpog toplevel *)
use "wfcpog_registry.sml";
use "wfcpog_constraint_library.sml";

4
su4sml/src/wfcpog/liskov_constraint.sml
View File

@ -71,6 +71,7 @@ struct
exception WFCPOG_LiskovError of string
(* su4sml *)
open HolOcl_Namespace
open Rep_Logger
open Rep_Core
open Rep_OclTerm
@ -120,7 +121,8 @@ 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,[mk_def_of ],(args2varargs (arguments_of_op op_of_super))))) (precondition_of_op op_of_super))
val term_super = conjugate_terms (List.map (fn (a,b) => (Predicate(b,type_of_term b,[]
(* [mk_def_of ] *),(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,[("dummy_name")],(args2varargs (arguments_of_op oper))))) (precondition_of_op oper))
in

8
su4sml/src/wfcpog/wfcpog_registry.sml
View File

@ -41,11 +41,11 @@
signature WFCPOG_REGISTRY =
sig
(*
structure WFCPOG_LSK_Data : WFCPOG_DATA
structure WFCPOG_TAX_Data : WFCPOG_DATA
structure WFCPOG_RFM_Data : WFCPOG_DATA
*)
val supported : WFCPOG.wfpo list
val wfpos : WFCPOG.wfpo list ref
@ -68,11 +68,11 @@ structure WFCPOG_Registry :WFCPOG_REGISTRY =
struct
exception WFCPOG_RegistryError of string
(*
structure WFCPOG_LSK_Data = WFCPOG_Liskov_Constraint.WFCPOG_LSK_Data
structure WFCPOG_TAX_Data = WFCPOG_Taxonomy_Constraint.WFCPOG_TAX_Data
structure WFCPOG_RFM_Data = WFCPOG_Refine_Constraint.WFCPOG_RFM_Data
*)
open Rep_Logger
open WFCPOG