Up to index of Isabelle/HOL/HOL-Z
theory ZMethod
(*************************************************************************)
(* Title : ZMethod.thy *)
(* Project : Z for Isabelle/HOL*)
(* Author : A.Brucker, ALU Freiburg, ETH Zürich *)
(* B. Wolff, BISS, ALU Freiburg, ETH Zürich *)
(* This File : Method Package for Z Specification *)
(* $Id: Z.thy,v 1.7 2002/08/05 10:18:56 wolff Exp $ *)
(* Copyright : ETH Zürich *)
(* Version : 3.0 *)
(*************************************************************************)
(* ML{*path_add "./lib"; *} *)
header {* Method Package for Z Representation and Z Refinement *}
theory ZMethod
imports ZPure
uses "ProofObligationMgr.sml"
begin
section {* Configuring the Generic PO Manager *}
ML{*
structure FMethod (*: FMETHOD*) =
struct
open POKind
val PO_classifier = Symtab.make[("tcc", repr),
("axdefConservative", lethal),
("ccState", wff),
("ccOp", wff),
("fwRefinementFunctional",meth),
("fwRefinementInit", meth),
("fwRefinementOp", meth)]
datatype content = Mk of {abs : (string*string*string) option,
functional_refinement : bool}
val init = Mk{abs = NONE,functional_refinement=false}
val merge = fn (x,y) => init
fun boolToString x = if x then "true" else "false"
fun print (Mk{abs,functional_refinement}) =
(writeln ("Method Package State:");
writeln ("=====================");
writeln ("abstraction relation: "^
(case abs of NONE => "---" | SOME (x,y,z) => x));
writeln ("functional refinemt : "^
(boolToString functional_refinement)))
end
structure ZPO_Mgr = PO_Manager (FMethod);
*}
text{* Initialize Environment *}
setup "ZPO_Mgr.PO_state_setup "
section{* The Z Method Package *}
text{* On top of the generic PO Manager, which has now been
imported and instantiated, we define a number of Method-
specific PO generation methods. In our case, we implement
support for classical forward data refinement (with an
optimizing option for functional abstraction relations)
following the lines described in the Spivey-Book also
described in the Woodcock/Davis Book "Using Z".
There is a general configuration operation \verb+set_abs+
that sets the underlying abstration relation and
concepts such as abstract or concrete state.
PO generators are in particular:
\begin{enumerate}
\item \verb+gen_state_cc+ for checking that state schemas
(representing system invariants) are in fact satisfyable.
\item \verb+gen_op_cc+ for checking that operation schemas
are "implementable" or "non-blocking", i.e. there exists a function
that maps inputs and state to outputs and successor state.
(Note that this function is \textbf{not} necessarily
computable).
\item \verb+gen_thm_tcc+ extracts from an arbitrary definition
or axiom the side-conditions for type-constraint-consistency.
(a representational side-condition of HOL-Z).
\item \verb+declare_abs+ allows for setting the
abstraction relation (per schema definition).
An additional option \verb+[functional]+ specifies
the relation to be functional, which results in different
(usually simpler) proof obligations.
\item \verb+refine_init+ for generating a PO assuring
compatibility of Init schemas (in forward simulation)
\item \verb+refine_op+ for generating two PO's establishing
refinement of operation schemas.
\end{enumerate}
*}
ML{*
signature ZMETHOD_PACKAGE =
sig
type schema_name = string
val gen_tcc_from : string -> theory -> theory
(* PRE string denotes thm which is schema_def or axdef.
POST add PO for each C(F%^E): CONT(C, F : Domain E)
*)
val gen_cc_state : schema_name -> theory -> theory
(* PRE stateschema is schema without x?, x!, x' variables.
POST add PO : ∃ x. x : stateschema *)
val gen_cc_op : schema_name -> theory -> theory
(* PRE opschema is schema with x and x' variables.
POST add PO : \<Sforall> state.∀ in.\<Sexists> state.
∃ out. op
*)
val declare_abs : bool -> schema_name -> theory -> theory
(* PRE absname must denote Z schema,
which imports exactly two schemas.
The first is used as abstract state,
the second as concrete state.
POST if functional,
add PO: "\<Sforall> state_conc. \<Sexists1> abs_state. abs"
else SKIP
*)
val refine_init : schema_name * schema_name -> theory -> theory
(* PRE abs relation must be set.
init_abs init_conc must be schema names.
POST if functional:
add PO:"\<Sforall> state_abs state_conc.
conc_init & abs \implies abs_init"
else add PO:"\<Sforall> state_conc. init_conc
\implies (\<Sexists> state_abs.
init_abs & abs)"
*)
val refine_ops : schema_name * schema_name -> theory -> theory
(* PRE abs relation must be set.
op_abs op_conc must be schema names.
POST if functional:
add PO: \<Sforall> state_abs state_conc. ∀ in.
pre op_abs ∧ abs --> pre op_conc
add PO: \<Sforall> state_abs state_conc. ∀ in out.
pre op_abs ∧ abs ∧ op_conc ∧ abs'
--> op_abs
else
add PO: \<Sforall> state_abs state_conc. ∀ in. pre op_abs
& abs --> pre op_conc
add PO: \<Sforall> abs_state conc_state. ∀ in out.
pre op_abs ∧ abs ∧ op_conc -->
\<Sexists> state_abs'. abs' ∧ op_abs
*)
end
*}
ML{*
structure ZMethod_Package : ZMETHOD_PACKAGE =
struct
val DEBUG = ref([]: string list)
type schema_name = string
fun gen_tcc_from name thy = error("NOT YET IMPLEMENTED")
fun is_schema name thy =
ZEnv.is_def(ZEnv.schemas_of (ZTheory.get_zenv thy),name)
fun gen_cc_state stateschema thy =
let val _ = if is_schema stateschema thy then ()
else error("Must be schema name: "^stateschema)
val zsig_opt= ZEnv.lookup (schemas_of(ZTheory.get_zenv thy),stateschema)
val nn= map fst (filter(fn (x,_) => ZPrelude.is_in_name x orelse
ZPrelude.is_out_name x orelse
ZPrelude.is_stroke_name x)
(schemasig_of(the zsig_opt)))
val _ = if null nn then ()
else error("state schema should contain only \
\undecorated variables: "^(String.concat nn))
val _ = (ZEncoder.ZENV:=ZTheory.get_zenv thy)
val agoal= "%E "^ stateschema^" @ True";
val cf = cterm_of(sign_of thy)
(ZEncoder.schema_read thy agoal)
val thy' = ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy),
"ccState",stateschema)
cf thy
val _ = writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf thy')))
in thy'
end
fun gen_cc_op opschema thy =
let val _ = if is_schema opschema thy then ()
else error("Must be schema name: "^opschema)
val zsig_opt= ZEnv.lookup (schemas_of(ZTheory.get_zenv thy),opschema)
val nn = map fst (filter(fn (x,_) => ZPrelude.is_stroke_name x)
(schemasig_of(the zsig_opt)))
val _ = if not(null nn) then ()
else error("op schema should contain \
\post state (i.e. 'stroked') components. ")
val _ = (ZEncoder.ZENV:=ZTheory.get_zenv thy)
val agoal= "pre "^ opschema;
val cf = cterm_of(sign_of thy)
(ZEncoder.schema_read thy agoal)
val thy' = ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy),
"ccOp",opschema)
cf thy
val _ = writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf thy')))
in thy'
end
fun declare_abs functional abs thy =
let
val _ = if is_schema abs thy then ()
else error("Must be schema name: "^abs)
val abs_term = concl_of (get_thm thy (Name(abs^"_def")))
val schema = ZEncoder.strip_Binder
(case abs_term of
Const("==",_) $ _ $ t => t
| _ => error("name must denote schema!"))
val decl = (case schema of
Const("ZPure.DECL",_) $ H $ _ => H
|_ => error("name must denote schema!"))
fun strip_sname (Const("ZPure.SNAME",_)$(Const(s,_))$_) = s
|strip_sname _ = error("declaration part must consist of \
\two schema names only!")
val (state_abs,state_conc) = (case decl of
Const ("op &", _)$H$H' => (strip_sname H,
strip_sname H')
| _ => error("declaration part must consist of \
\two schema names only!"))
val cont = FMethod.Mk{abs=SOME(abs,
(NameSpace.base state_abs),
(NameSpace.base state_conc)),
functional_refinement=functional}
val thy' = ZPO_Mgr.set_content cont thy
val _ = (ZEncoder.ZENV:=ZTheory.get_zenv thy');
val agoal= "%A "^(NameSpace.base state_conc)^" @ (%E1 "^
(NameSpace.base state_abs)^" @ "^(NameSpace.base abs)^")";
val cf = cterm_of(sign_of thy')
(ZEncoder.schema_read thy' agoal)
val thy''= if functional
then ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy'),
"fwRefinementFunctional",abs)
cf thy'
else thy'
val _ = if functional
then writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf thy'')))
else ()
in thy'' end
fun refine_init(init_abs, init_conc)(thy) =
let val _ = if is_schema init_abs thy then ()
else error("Must be schema name: "^init_abs)
val _ = if is_schema init_conc thy then ()
else error("Must be schema name: "^init_conc)
val FMethod.Mk{abs,functional_refinement} = ZPO_Mgr.get_content thy
val (abs, state_abs, state_conc)= case abs of
NONE => error"no abstraction relation set!"
| SOME x => x
val term_abs = concl_of (get_thm thy (Name(init_abs^"_def")))
val term_conc = concl_of (get_thm thy (Name(init_conc^"_def")))
val term_abs = ZEncoder.strip_Binder
(case term_abs of
Const("==",_) $ _ $ t => t
| _ => error(init_abs^"must denote init schema!"))
val term_conc = ZEncoder.strip_Binder
(case term_conc of
Const("==",_) $ _ $ t => t
| _ => error(init_conc^"must denote init schema!"))
fun test m (Const("ZPure.DECL",_)
$ (Const("ZPure.SNAME",_) $ Const(s,_) $_)
$ _) =
if (NameSpace.base s) = m then ()
else error("imported schema must be :"^m)
|test m _ = error"illegal pattern of import schema"
val _ = test state_abs term_abs
val _ = test state_conc term_conc
val goal = if functional_refinement
then "%A "^state_abs^" @ (%A "^state_conc^" @ ("
^ init_conc ^" & "^abs^" --> "^init_abs^"))"
else "%A "^state_conc^" @ ("^ init_conc ^" --> "^
"(%E "^state_abs^" @ ("^abs^" & "^init_abs^")))"
val cf = cterm_of(sign_of thy)
(ZEncoder.schema_read thy goal)
val thy' = ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy),
"fwRefinementInit",state_abs)
cf thy
val _ = writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf thy')))
in thy' end
fun refine_ops (op_abs, op_conc) thy =
let (* checking syntactic side-conditions ... *)
val _ = if is_schema op_abs thy then ()
else error("Must be schema name: "^op_abs)
val _ = if is_schema op_conc thy then ()
else error("Must be schema name: "^op_conc)
val FMethod.Mk{abs,functional_refinement} = ZPO_Mgr.get_content thy
val SOME(abs, state_abs, state_conc)=abs
val term_abs = concl_of (get_thm thy (Name(op_abs^"_def")))
val term_conc = concl_of (get_thm thy (Name(op_conc^"_def")))
val term_abs = ZEncoder.strip_Binder
(case term_abs of
Const("==",_) $ _ $ t => t
| _ => error(op_abs^"must denote op schema!"))
val term_conc = ZEncoder.strip_Binder
(case term_conc of
Const("==",_) $ _ $ t => t
| _ => error(op_conc^"must denote op schema!"))
fun test m (Const("ZPure.DECL",_) $
(Const ("op &",_)
$ (Const ("ZPure.DELTA",_)
$ (Const("ZPure.SNAME",_)$(Const(s,_))$_)
$ _)
$ _) $ _) =
(if (NameSpace.base s) = m then ()
else error("imported schema must be :"^m))
|test m (Const("ZPure.DECL",_) $
(Const ("op &",_)
$ (Const ("ZPure.DELTA",_)
$ (Const ("ZPure.DELTA",_)
$ (Const("ZPure.SNAME",_)$(Const(s,_))$_)
$ _)
$ _ $ _)
$ _) $ _) =
(if (NameSpace.base s) = m then ()
else error("imported schema must be :"^m))
|test m _ = error("illegal pattern of schema:"^m)
val _ = test state_abs term_abs
val _ = test state_conc term_conc
fun zsig_of name = schemasig_of(the(ZEnv.lookup
(schemas_of(ZTheory.get_zenv thy),name)))
fun get_params test name = filter test
(map fst (zsig_of name))
val in_parms = get_params ZPrelude.is_in_name op_abs
val in_parms' = get_params ZPrelude.is_in_name op_conc
val _ = if in_parms = in_parms' then ()
else error("Input parameters must agree !")
val out_parms = get_params ZPrelude.is_out_name op_abs
val out_parms'= get_params ZPrelude.is_out_name op_conc
val _ = if out_parms = out_parms' then ()
else error("Output parameters must agree !")
(* generating proof obligations ... *)
fun ALL [] b = "("^b^")"
|ALL S b = "(ALL "^(String.concat
(map(fn x => x^" ")S))^". "^b^")"
val goal1 = "%A "^state_abs^" @ (%A "^state_conc^" @ "^
(ALL in_parms
("pre "^op_abs^" ∧ "^abs^
" --> pre "^op_conc))^")"
val goal2c= if functional_refinement
then " ∧ "^abs^"' --> "^op_abs
else " --> (%E "^state_abs^"' @ "
^abs^"' ∧ "^op_abs^")"
val goal2a= "%A "^state_abs^" @ (%A "^state_conc^" @ "^
"(%A "^state_conc^"' @ "^
(ALL in_parms
(ALL out_parms ("pre "^op_abs^" ∧ "^abs^
" ∧ "^op_conc^
" --> (%E "
^state_abs^"' @ "^abs^
"' ∧ "^op_abs^")")))^"))"
val goal2b= "%A "^state_abs^" @ (%A "^state_abs^
"' @ (%A "^state_conc^" @ "^ "(%A "^state_conc^"' @ "^
(ALL in_parms
(ALL out_parms ("pre "^op_abs^" ∧ "^abs^
" ∧ "^op_conc^
" ∧ "^abs^
"' --> "^op_abs
)))^")))"
val goal2 = if functional_refinement then goal2b else goal2a
val cf1 = cterm_of(sign_of thy)
(ZEncoder.schema_read thy goal1)
val cf2 = cterm_of(sign_of thy)
(ZEncoder.schema_read thy goal2)
val thy' = ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy),
"fwRefinementOp",op_abs)
cf1 thy
val thy'' = ZPO_Mgr.declare_PO
(SOME(Context.theory_name thy),
"fwRefinementOp",op_abs)
cf2 thy'
val _ = writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf1 thy'')))
val _ = writeln("PO declared: "^(the
(ZPO_Mgr.get_name_of_PO cf2 thy'')))
in thy'' end
structure P = OuterParse and K = OuterKeyword;
val declare_absP =
let fun declare_abs'(name,X) = declare_abs (isSome X) name
in OuterSyntax.command "set_abs" "set abstraction relation"
OuterKeyword.thy_script
((P.name) -- (Scan.option (P.$$$ "[" |-- P.$$$ "functional" --| P.$$$ "]"))
>> (Toplevel.theory o declare_abs'))
end;
val _ = OuterSyntax.add_parsers [declare_absP];
val _ = OuterSyntax.add_keywords ["functional"];
val gen_tcc_fromP =
OuterSyntax.command "gen_thm_tcc" "generate type constraint side conditions"
OuterKeyword.thy_script
((P.name) >> (Toplevel.theory o gen_tcc_from));
val _ = OuterSyntax.add_parsers [gen_tcc_fromP];
val gen_cc_stateP =
OuterSyntax.command "gen_state_cc" "generate state consistency conditions"
OuterKeyword.thy_script
((P.name) >> (Toplevel.theory o gen_cc_state));
val _ = OuterSyntax.add_parsers [gen_cc_stateP];
val gen_cc_opP =
OuterSyntax.command "gen_op_cc" "generate operation consistency relation"
OuterKeyword.thy_script
((P.name) >> (Toplevel.theory o gen_cc_op));
val _ = OuterSyntax.add_parsers [gen_cc_opP];
val refine_opsP =
OuterSyntax.command "refine_op" "generate forward refinement proof obligations"
OuterKeyword.thy_script
((P.name) -- (P.name) >> (Toplevel.theory o refine_ops));
val _ = OuterSyntax.add_parsers [refine_opsP];
val refine_initP =
OuterSyntax.command "refine_init" "generate forward refinement proof obligations for init schemas"
OuterKeyword.thy_script
((P.name) -- (P.name) >> (Toplevel.theory o refine_init));
val _ = OuterSyntax.add_parsers [refine_initP];
end
*}
end