# HG changeset patch # User nipkow # Date 822391175 -3600 # Node ID bc2c0acbbf29c17440240fbf82fd41a205bf42f7 # Parent a8387e934fa71f94efc5d2af2a402ebcdd992d98 Added a verified verification-condition generator. diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/Hoare.ML --- a/src/HOL/IMP/Hoare.ML Sat Jan 20 02:00:11 1996 +0100 +++ b/src/HOL/IMP/Hoare.ML Tue Jan 23 10:59:35 1996 +0100 @@ -3,55 +3,28 @@ Author: Tobias Nipkow Copyright 1995 TUM -Derivation of Hoare rules +Soundness of Hoare rules wrt denotational semantics *) open Hoare; -Unify.trace_bound := 30; -Unify.search_bound := 30; - -goalw Hoare.thy [spec_def] - "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \ -\ ==> {{P'}}c{{Q'}}"; -by(fast_tac HOL_cs 1); -bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result()))); - -goalw Hoare.thy (spec_def::C_simps) "{{P}} skip {{P}}"; -by(fast_tac comp_cs 1); -qed"hoare_skip"; - -goalw Hoare.thy (spec_def::C_simps) - "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}"; -by(Asm_full_simp_tac 1); -qed"hoare_assign"; - -goalw Hoare.thy (spec_def::C_simps) - "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}"; -by(fast_tac comp_cs 1); -qed"hoare_seq"; - -goalw Hoare.thy (spec_def::C_simps) - "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \ -\ {{P}} ifc b then c else d {{Q}}"; -by(Simp_tac 1); -by(fast_tac comp_cs 1); -qed"hoare_if"; - -goalw Hoare.thy (spec_def::C_simps) - "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \ -\ {{P}} while b do c {{%s. P s & ~B b s}}"; +goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; +br hoare.mutual_induct 1; + by(ALLGOALS Asm_simp_tac); + by(fast_tac rel_cs 1); + by(fast_tac HOL_cs 1); br allI 1; br allI 1; br impI 1; be induct2 1; -br Gamma_mono 1; + br Gamma_mono 1; by (rewrite_goals_tac [Gamma_def]); by(eres_inst_tac [("x","a")] allE 1); by (safe_tac comp_cs); -by(ALLGOALS Asm_full_simp_tac); -qed"hoare_while"; + by(ALLGOALS Asm_full_simp_tac); +qed "hoare_sound"; +(* fun while_tac inv ss i = EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i, asm_full_simp_tac ss (i+1)]; @@ -75,3 +48,4 @@ by(while_tac "%s.s z = i + s u & s y = j" ss 3); by(hoare_tac ss); result(); +*) diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Sat Jan 20 02:00:11 1996 +0100 +++ b/src/HOL/IMP/Hoare.thy Tue Jan 23 10:59:35 1996 +0100 @@ -3,47 +3,32 @@ Author: Tobias Nipkow Copyright 1995 TUM -Semantic embedding of Hoare logic +Inductive definition of Hoare logic *) Hoare = Denotation + + +types assn = state => bool + consts + hoare :: "(assn * com * assn) set" spec :: [state=>bool,com,state=>bool] => bool -(* syntax "@spec" :: [bool,com,bool] => bool *) - ("{{(1_)}}/ (_)/ {{(1_)}}" 10) defs spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t" -end -(* Pretty-printing of assertions. - Not very helpful as long as programs are not pretty-printed. -ML -local open Syntax - -fun is_loc a = let val ch = hd(explode a) - in ord "A" <= ord ch andalso ord ch <= ord "Z" end; - -fun tr(s$t,i) = tr(s,i)$tr(t,i) - | tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1)) - | tr(t as Free(a,T),i) = if is_loc a then Bound(i) $ free(a) else t - | tr(t,_) = t; +syntax "@hoare" :: [bool,com,bool] => bool ("{{(1_)}}/ (_)/ {{(1_)}}" 10) +translations "{{P}}c{{Q}}" == "(P,c,Q) : hoare" -fun cond_tr(p) = Abs("",dummyT,tr(p,0)) - -fun spec_tr[p,c,q] = const"spec" $ cond_tr p $ c $ cond_tr q; - -fun tr'(t as (Bound j $ (u as Free(a,_))),i) = if i=j then u else t - | tr'(s$t,i) = tr'(s,i)$tr'(t,i) - | tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1)) - | tr'(t,_) = t; - -fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] = - const"@spec" $ tr'(p,0) $ c $ tr'(q,0); - -in - -val parse_translation = [("@spec", spec_tr)]; -val print_translation = [("spec", spec_tr')]; +inductive "hoare" +intrs + hoare_skip "{{P}}skip{{P}}" + hoare_ass "{{%s.P(s[A a s/x])}} x:=a {{P}}" + hoare_semi "[| {{P}}c{{Q}}; {{Q}}d{{R}} |] ==> {{P}} c;d {{R}}" + hoare_if "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==> + {{P}} ifc b then c else d {{Q}}" + hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==> + {{P}} while b do c {{%s. P s & ~B b s}}" + hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==> + {{P'}}c{{Q'}}" end -*) diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/README.html --- a/src/HOL/IMP/README.html Sat Jan 20 02:00:11 1996 +0100 +++ b/src/HOL/IMP/README.html Tue Jan 23 10:59:35 1996 +0100 @@ -1,20 +1,21 @@ HOL/IMP/ReadMe -

IMP --- A while-Language and its 3 Semantics

+

IMP --- A while-language and its 3 Semantics

The formalization of the denotational, operational and axiomatic semantics of a simple while-language, including The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of

-@book{Winskel,author={Glynn Winskel}, -title={The Formal Semantics of Programming Languages}, -publisher={MIT Press},year=1993} +@book{Winskel, author = {Glynn Winskel}, +title = {The Formal Semantics of Programming Languages}, +publisher = {MIT Press}, year = 1993}

-Here is the documentation. +In addition, a verification-condition-generator is proved sound and complete +w.r.t. the Hoare rules. diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/ROOT.ML --- a/src/HOL/IMP/ROOT.ML Sat Jan 20 02:00:11 1996 +0100 +++ b/src/HOL/IMP/ROOT.ML Tue Jan 23 10:59:35 1996 +0100 @@ -10,4 +10,4 @@ proof_timing := true; time_use_thy "Properties"; time_use_thy "Equiv"; -time_use_thy "Hoare"; +time_use_thy "VC"; diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/VC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/VC.ML Tue Jan 23 10:59:35 1996 +0100 @@ -0,0 +1,79 @@ +(* Title: HOL/IMP/VC.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1996 TUM + +Soundness and completeness of vc +*) + +open VC; + +val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]); + +goal VC.thy "!Q. (!s. vc c Q s) --> ({{wp c Q}} (astrip c) {{Q}})"; +by(acom.induct_tac "c" 1); + by(ALLGOALS Simp_tac); + by(fast_tac (HOL_cs addIs hoare.intrs) 1); + by(fast_tac (HOL_cs addIs hoare.intrs) 1); + by(fast_tac (HOL_cs addIs hoare.intrs) 1); + (* if *) + br allI 1; + br impI 1; + brs hoare.intrs 1; + brs hoare.intrs 1; + by(fast_tac HOL_cs 2); + by(fast_tac HOL_cs 1); + by(fast_tac HOL_cs 1); + brs hoare.intrs 1; + by(fast_tac HOL_cs 2); + by(fast_tac HOL_cs 1); + by(fast_tac HOL_cs 1); +(* while *) +by(safe_tac HOL_cs); +brs hoare.intrs 1; + br lemma 1; + brs hoare.intrs 1; + brs hoare.intrs 1; + by(fast_tac HOL_cs 2); + by(ALLGOALS(fast_tac HOL_cs)); +qed "vc_sound"; + +goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)"; +by(acom.induct_tac "c" 1); + by(ALLGOALS Asm_simp_tac); +by(EVERY1[rtac allI, rtac allI, rtac impI]); +by(EVERY1[etac allE, etac allE, etac mp]); +by(EVERY1[etac allE, etac allE, etac mp, atac]); +bind_thm("wp_mono", result() RS spec RS spec RS mp RS spec RS mp); + +goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"; +by(acom.induct_tac "c" 1); + by(ALLGOALS Asm_simp_tac); +by(safe_tac HOL_cs); +by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); +by(fast_tac (HOL_cs addEs [wp_mono]) 1); +bind_thm("vc_mono", result() RS spec RS spec RS mp RS spec RS mp); + +goal VC.thy + "!P c Q. ({{P}}c{{Q}}) --> \ +\ (? ac. astrip ac = c & (!s. P s --> wp ac Q s) & (!s. vc ac Q s))"; +br hoare.mutual_induct 1; + by(res_inst_tac [("x","Askip")] exI 1); + by(Simp_tac 1); + by(res_inst_tac [("x","Aass x a")] exI 1); + by(Simp_tac 1); + by(SELECT_GOAL(safe_tac HOL_cs)1); + by(res_inst_tac [("x","Asemi ac aca")] exI 1); + by(Asm_simp_tac 1); + by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); + by(SELECT_GOAL(safe_tac HOL_cs)1); + by(res_inst_tac [("x","Aif b ac aca")] exI 1); + by(Asm_simp_tac 1); + by(SELECT_GOAL(safe_tac HOL_cs)1); + by(res_inst_tac [("x","Awhile b P ac")] exI 1); + by(Asm_simp_tac 1); +by(SELECT_GOAL(safe_tac HOL_cs)1); +by(res_inst_tac [("x","ac")] exI 1); +by(Asm_simp_tac 1); +by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); +qed "vc_complete"; diff -r a8387e934fa7 -r bc2c0acbbf29 src/HOL/IMP/VC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IMP/VC.thy Tue Jan 23 10:59:35 1996 +0100 @@ -0,0 +1,45 @@ +(* Title: HOL/IMP/VC.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1996 TUM + +acom: annotated commands +vc: verification-conditions +wp: weakest (liberal) precondition +*) + +VC = Hoare + + +datatype acom = Askip + | Aass loc aexp + | Asemi acom acom + | Aif bexp acom acom + | Awhile bexp assn acom + +consts + vc,wp :: acom => assn => assn + astrip :: acom => com + +primrec wp acom + wp_Askip "wp Askip Q = Q" + wp_Aass "wp (Aass x a) Q = (%s.Q(s[A a s/x]))" + wp_Asemi "wp (Asemi c d) Q = wp c (wp d Q)" + wp_Aif "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" + wp_Awhile "wp (Awhile b I c) Q = I" + +primrec vc acom + vc_Askip "vc Askip Q = (%s.True)" + vc_Aass "vc (Aass x a) Q = (%s.True)" + vc_Asemi "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)" + vc_Aif "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" + vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) & + (I s & B b s --> wp c I s) & vc c I s)" + +primrec astrip acom + astrip_Askip "astrip Askip = skip" + astrip_Aass "astrip (Aass x a) = (x:=a)" + astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" + astrip_Aif "astrip (Aif b c d) = ifC b (astrip c) (astrip d)" + astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)" + +end