Added a verified verification-condition generator.
authornipkow
Tue Jan 23 10:59:35 1996 +0100 (1996-01-23)
changeset 1447bc2c0acbbf29
parent 1446 a8387e934fa7
child 1448 77379ae9ff0d
Added a verified verification-condition generator.
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/README.html
src/HOL/IMP/ROOT.ML
src/HOL/IMP/VC.ML
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/Hoare.ML	Sat Jan 20 02:00:11 1996 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.ML	Tue Jan 23 10:59:35 1996 +0100
     1.3 @@ -3,55 +3,28 @@
     1.4      Author: 	Tobias Nipkow
     1.5      Copyright   1995 TUM
     1.6  
     1.7 -Derivation of Hoare rules
     1.8 +Soundness of Hoare rules wrt denotational semantics
     1.9  *)
    1.10  
    1.11  open Hoare;
    1.12  
    1.13 -Unify.trace_bound := 30;
    1.14 -Unify.search_bound := 30;
    1.15 -
    1.16 -goalw Hoare.thy [spec_def]
    1.17 -  "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \
    1.18 -\  ==> {{P'}}c{{Q'}}";
    1.19 -by(fast_tac HOL_cs 1);
    1.20 -bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result())));
    1.21 -
    1.22 -goalw Hoare.thy (spec_def::C_simps)  "{{P}} skip {{P}}";
    1.23 -by(fast_tac comp_cs 1);
    1.24 -qed"hoare_skip";
    1.25 -
    1.26 -goalw Hoare.thy (spec_def::C_simps)
    1.27 -  "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}";
    1.28 -by(Asm_full_simp_tac 1);
    1.29 -qed"hoare_assign";
    1.30 -
    1.31 -goalw Hoare.thy (spec_def::C_simps)
    1.32 -  "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}";
    1.33 -by(fast_tac comp_cs 1);
    1.34 -qed"hoare_seq";
    1.35 -
    1.36 -goalw Hoare.thy (spec_def::C_simps)
    1.37 -  "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \
    1.38 -\  {{P}} ifc b then c else d {{Q}}";
    1.39 -by(Simp_tac 1);
    1.40 -by(fast_tac comp_cs 1);
    1.41 -qed"hoare_if";
    1.42 -
    1.43 -goalw Hoare.thy (spec_def::C_simps)
    1.44 -  "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
    1.45 -\  {{P}} while b do c {{%s. P s & ~B b s}}";
    1.46 +goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q";
    1.47 +br hoare.mutual_induct 1;
    1.48 +    by(ALLGOALS Asm_simp_tac);
    1.49 +  by(fast_tac rel_cs 1);
    1.50 + by(fast_tac HOL_cs 1);
    1.51  br allI 1;
    1.52  br allI 1;
    1.53  br impI 1;
    1.54  be induct2 1;
    1.55 -br Gamma_mono 1;
    1.56 + br Gamma_mono 1;
    1.57  by (rewrite_goals_tac [Gamma_def]);  
    1.58  by(eres_inst_tac [("x","a")] allE 1);
    1.59  by (safe_tac comp_cs);
    1.60 -by(ALLGOALS Asm_full_simp_tac);
    1.61 -qed"hoare_while";
    1.62 +  by(ALLGOALS Asm_full_simp_tac);
    1.63 +qed "hoare_sound";
    1.64  
    1.65 +(*
    1.66  fun while_tac inv ss i =
    1.67    EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
    1.68          asm_full_simp_tac ss (i+1)];
    1.69 @@ -75,3 +48,4 @@
    1.70  by(while_tac "%s.s z = i + s u & s y = j" ss 3);
    1.71  by(hoare_tac ss);
    1.72  result();
    1.73 +*)
     2.1 --- a/src/HOL/IMP/Hoare.thy	Sat Jan 20 02:00:11 1996 +0100
     2.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Jan 23 10:59:35 1996 +0100
     2.3 @@ -3,47 +3,32 @@
     2.4      Author: 	Tobias Nipkow
     2.5      Copyright   1995 TUM
     2.6  
     2.7 -Semantic embedding of Hoare logic
     2.8 +Inductive definition of Hoare logic
     2.9  *)
    2.10  
    2.11  Hoare = Denotation +
    2.12 +
    2.13 +types assn = state => bool
    2.14 +
    2.15  consts
    2.16 +  hoare :: "(assn * com * assn) set"
    2.17    spec :: [state=>bool,com,state=>bool] => bool
    2.18 -(* syntax "@spec" :: [bool,com,bool] => bool *)
    2.19 -          ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    2.20  defs
    2.21    spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
    2.22 -end
    2.23 -(* Pretty-printing of assertions.
    2.24 -   Not very helpful as long as programs are not pretty-printed.
    2.25 -ML
    2.26  
    2.27 -local open Syntax
    2.28 -
    2.29 -fun is_loc a = let val ch = hd(explode a)
    2.30 -               in ord "A" <= ord ch andalso ord ch <= ord "Z" end;
    2.31 -
    2.32 -fun tr(s$t,i) = tr(s,i)$tr(t,i)
    2.33 -  | tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1))
    2.34 -  | tr(t as Free(a,T),i) = if is_loc a then Bound(i) $ free(a) else t
    2.35 -  | tr(t,_) = t;
    2.36 +syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    2.37 +translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare"
    2.38  
    2.39 -fun cond_tr(p) = Abs("",dummyT,tr(p,0))
    2.40 -
    2.41 -fun spec_tr[p,c,q] = const"spec" $ cond_tr p $ c $ cond_tr q;
    2.42 -
    2.43 -fun tr'(t as (Bound j $ (u as Free(a,_))),i) = if i=j then u else t
    2.44 -  | tr'(s$t,i) = tr'(s,i)$tr'(t,i)
    2.45 -  | tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1))
    2.46 -  | tr'(t,_) = t;
    2.47 -
    2.48 -fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] =
    2.49 -  const"@spec" $ tr'(p,0) $ c $ tr'(q,0);
    2.50 -
    2.51 -in
    2.52 -
    2.53 -val parse_translation = [("@spec", spec_tr)];
    2.54 -val print_translation = [("spec", spec_tr')];
    2.55 +inductive "hoare"
    2.56 +intrs
    2.57 +  hoare_skip "{{P}}skip{{P}}"
    2.58 +  hoare_ass  "{{%s.P(s[A a s/x])}} x:=a {{P}}"
    2.59 +  hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}"
    2.60 +  hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    2.61 +              {{P}} ifc b then c else d {{Q}}"
    2.62 +  hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    2.63 +	       {{P}} while b do c {{%s. P s & ~B b s}}"
    2.64 +  hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    2.65 +		{{P'}}c{{Q'}}"
    2.66  
    2.67  end
    2.68 -*)
     3.1 --- a/src/HOL/IMP/README.html	Sat Jan 20 02:00:11 1996 +0100
     3.2 +++ b/src/HOL/IMP/README.html	Tue Jan 23 10:59:35 1996 +0100
     3.3 @@ -1,20 +1,21 @@
     3.4  <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
     3.5  
     3.6 -<H2>IMP --- A <KBD>while</KBD>-Language and its 3 Semantics</H2>
     3.7 +<H2>IMP --- A <KBD>while</KBD>-language and its 3 Semantics</H2>
     3.8  
     3.9  The formalization of the denotational, operational and axiomatic semantics of
    3.10  a simple while-language, including
    3.11  <UL>
    3.12  <LI> an equivalence proof between denotational and operational semantics and
    3.13 -<LI> the derivation of the Hoare rules from the denotational semantics.
    3.14 +<LI> a soundness proof of the Hoare rules w.r.t. the denotational semantics.
    3.15  </UL>
    3.16  The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
    3.17  <P>
    3.18  <KBD>
    3.19 -@book{Winskel,author={Glynn Winskel},
    3.20 -title={The Formal Semantics of Programming Languages},
    3.21 -publisher={MIT Press},year=1993}
    3.22 +@book{Winskel, author = {Glynn Winskel},
    3.23 +title = {The Formal Semantics of Programming Languages},
    3.24 +publisher = {MIT Press}, year = 1993}
    3.25  </KBD>
    3.26  <P>
    3.27 -Here is the documentation.
    3.28 +In addition, a verification-condition-generator is proved sound and complete
    3.29 +w.r.t. the Hoare rules.
    3.30  </BODY></HTML>
     4.1 --- a/src/HOL/IMP/ROOT.ML	Sat Jan 20 02:00:11 1996 +0100
     4.2 +++ b/src/HOL/IMP/ROOT.ML	Tue Jan 23 10:59:35 1996 +0100
     4.3 @@ -10,4 +10,4 @@
     4.4  proof_timing := true;
     4.5  time_use_thy "Properties";
     4.6  time_use_thy "Equiv";
     4.7 -time_use_thy "Hoare";
     4.8 +time_use_thy "VC";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/IMP/VC.ML	Tue Jan 23 10:59:35 1996 +0100
     5.3 @@ -0,0 +1,79 @@
     5.4 +(*  Title: 	HOL/IMP/VC.ML
     5.5 +    ID:         $Id$
     5.6 +    Author: 	Tobias Nipkow
     5.7 +    Copyright   1996 TUM
     5.8 +
     5.9 +Soundness and completeness of vc
    5.10 +*)
    5.11 +
    5.12 +open VC;
    5.13 +
    5.14 +val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]);
    5.15 +
    5.16 +goal VC.thy "!Q. (!s. vc c Q s) --> ({{wp c Q}} (astrip c) {{Q}})";
    5.17 +by(acom.induct_tac "c" 1);
    5.18 +    by(ALLGOALS Simp_tac);
    5.19 +    by(fast_tac (HOL_cs addIs hoare.intrs) 1);
    5.20 +   by(fast_tac (HOL_cs addIs hoare.intrs) 1);
    5.21 +  by(fast_tac (HOL_cs addIs hoare.intrs) 1);
    5.22 + (* if *)
    5.23 + br allI 1;
    5.24 + br impI 1;
    5.25 + brs hoare.intrs 1;
    5.26 +  brs hoare.intrs 1;
    5.27 +    by(fast_tac HOL_cs 2);
    5.28 +   by(fast_tac HOL_cs 1);
    5.29 +  by(fast_tac HOL_cs 1);
    5.30 + brs hoare.intrs 1;
    5.31 +   by(fast_tac HOL_cs 2);
    5.32 +  by(fast_tac HOL_cs 1);
    5.33 + by(fast_tac HOL_cs 1);
    5.34 +(* while *)
    5.35 +by(safe_tac HOL_cs);
    5.36 +brs hoare.intrs 1;
    5.37 +  br lemma 1;
    5.38 + brs hoare.intrs 1;
    5.39 + brs hoare.intrs 1;
    5.40 +   by(fast_tac HOL_cs 2);
    5.41 +  by(ALLGOALS(fast_tac HOL_cs));
    5.42 +qed "vc_sound";
    5.43 +
    5.44 +goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
    5.45 +by(acom.induct_tac "c" 1);
    5.46 +    by(ALLGOALS Asm_simp_tac);
    5.47 +by(EVERY1[rtac allI, rtac allI, rtac impI]);
    5.48 +by(EVERY1[etac allE, etac allE, etac mp]);
    5.49 +by(EVERY1[etac allE, etac allE, etac mp, atac]);
    5.50 +bind_thm("wp_mono", result() RS spec RS spec RS mp RS spec RS mp);
    5.51 +
    5.52 +goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
    5.53 +by(acom.induct_tac "c" 1);
    5.54 +    by(ALLGOALS Asm_simp_tac);
    5.55 +by(safe_tac HOL_cs);
    5.56 +by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
    5.57 +by(fast_tac (HOL_cs addEs [wp_mono]) 1);
    5.58 +bind_thm("vc_mono", result() RS spec RS spec RS mp RS spec RS mp);
    5.59 +
    5.60 +goal VC.thy
    5.61 +  "!P c Q. ({{P}}c{{Q}}) --> \
    5.62 +\          (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))";
    5.63 +br hoare.mutual_induct 1;
    5.64 +     by(res_inst_tac [("x","Askip")] exI 1);
    5.65 +     by(Simp_tac 1);
    5.66 +    by(res_inst_tac [("x","Aass x a")] exI 1);
    5.67 +    by(Simp_tac 1);
    5.68 +   by(SELECT_GOAL(safe_tac HOL_cs)1);
    5.69 +   by(res_inst_tac [("x","Asemi ac aca")] exI 1);
    5.70 +   by(Asm_simp_tac 1);
    5.71 +   by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
    5.72 +  by(SELECT_GOAL(safe_tac HOL_cs)1);
    5.73 +  by(res_inst_tac [("x","Aif b ac aca")] exI 1);
    5.74 +  by(Asm_simp_tac 1);
    5.75 + by(SELECT_GOAL(safe_tac HOL_cs)1);
    5.76 + by(res_inst_tac [("x","Awhile b P ac")] exI 1);
    5.77 + by(Asm_simp_tac 1);
    5.78 +by(SELECT_GOAL(safe_tac HOL_cs)1);
    5.79 +by(res_inst_tac [("x","ac")] exI 1);
    5.80 +by(Asm_simp_tac 1);
    5.81 +by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
    5.82 +qed "vc_complete";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/IMP/VC.thy	Tue Jan 23 10:59:35 1996 +0100
     6.3 @@ -0,0 +1,45 @@
     6.4 +(*  Title: 	HOL/IMP/VC.thy
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Tobias Nipkow
     6.7 +    Copyright   1996 TUM
     6.8 +
     6.9 +acom: annotated commands
    6.10 +vc:   verification-conditions
    6.11 +wp:   weakest (liberal) precondition
    6.12 +*)
    6.13 +
    6.14 +VC  =  Hoare +
    6.15 +
    6.16 +datatype  acom = Askip
    6.17 +               | Aass   loc aexp
    6.18 +               | Asemi  acom acom
    6.19 +               | Aif    bexp acom acom
    6.20 +               | Awhile bexp assn acom
    6.21 +
    6.22 +consts
    6.23 +  vc,wp :: acom => assn => assn
    6.24 +  astrip :: acom => com
    6.25 +
    6.26 +primrec wp acom
    6.27 +  wp_Askip  "wp Askip Q = Q"
    6.28 +  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
    6.29 +  wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
    6.30 +  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
    6.31 +  wp_Awhile "wp (Awhile b I c) Q = I"
    6.32 +
    6.33 +primrec vc acom
    6.34 +  vc_Askip  "vc Askip Q = (%s.True)"
    6.35 +  vc_Aass   "vc (Aass x a) Q = (%s.True)"
    6.36 +  vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
    6.37 +  vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
    6.38 +  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
    6.39 +                              (I s & B b s --> wp c I s) & vc c I s)"
    6.40 +
    6.41 +primrec astrip acom
    6.42 +  astrip_Askip  "astrip Askip = skip"
    6.43 +  astrip_Aass   "astrip (Aass x a) = (x:=a)"
    6.44 +  astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
    6.45 +  astrip_Aif    "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
    6.46 +  astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
    6.47 +  
    6.48 +end