|
1 (* Title: HOL/IMPP/Hoare.thy |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb |
|
4 Copyright 1999 TUM |
|
5 |
|
6 Inductive definition of Hoare logic for partial correctness |
|
7 Completeness is taken relative to completeness of the underlying logic |
|
8 Two versions of completeness proof: |
|
9 nested single recursion vs. simultaneous recursion in call rule |
|
10 *) |
|
11 |
|
12 Hoare = Natural + |
|
13 |
|
14 types 'a assn = "'a => state => bool" |
|
15 translations |
|
16 "a assn" <= (type)"a => state => bool" |
|
17 |
|
18 constdefs |
|
19 state_not_singleton :: bool |
|
20 "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *) |
|
21 |
|
22 peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) |
|
23 "peek_and P p == %Z s. P Z s & p s" |
|
24 |
|
25 datatype 'a triple = |
|
26 triple ('a assn) com ('a assn) ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) |
|
27 |
|
28 consts |
|
29 triple_valid :: nat => 'a triple => bool ( "|=_:_" [0 , 58] 57) |
|
30 hoare_valids :: 'a triple set => 'a triple set => bool ("_||=_" [58, 58] 57) |
|
31 hoare_derivs ::"('a triple set * 'a triple set) set" |
|
32 syntax |
|
33 triples_valid:: nat => 'a triple set => bool ("||=_:_" [0 , 58] 57) |
|
34 hoare_valid :: 'a triple set => 'a triple => bool ("_|=_" [58, 58] 57) |
|
35 "@hoare_derivs":: 'a triple set => 'a triple set => bool ("_||-_" [58, 58] 57) |
|
36 "@hoare_deriv" :: 'a triple set => 'a triple => bool ("_|-_" [58, 58] 57) |
|
37 |
|
38 defs triple_valid_def "|=n:t == case t of {P}.c.{Q} => |
|
39 !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')" |
|
40 translations "||=n:G" == "Ball G (triple_valid n)" |
|
41 defs hoare_valids_def"G||=ts == !n. ||=n:G --> ||=n:ts" |
|
42 translations "G |=t " == " G||={t}" |
|
43 "G||-ts" == "(G,ts) : hoare_derivs" |
|
44 "G |-t" == " G||-{t}" |
|
45 |
|
46 (* Most General Triples *) |
|
47 constdefs MGT :: com => state triple ("{=}._.{->}" [60] 58) |
|
48 "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" |
|
49 |
|
50 inductive hoare_derivs intrs |
|
51 |
|
52 empty "G||-{}" |
|
53 insert"[| G |-t; G||-ts |] |
|
54 ==> G||-insert t ts" |
|
55 |
|
56 asm "ts <= G ==> |
|
57 G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) |
|
58 |
|
59 cut "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) |
|
60 |
|
61 weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts" |
|
62 |
|
63 conseq"!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} & |
|
64 (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s')) |
|
65 ==> G|-{P}.c.{Q}" |
|
66 |
|
67 |
|
68 Skip "G|-{P}. SKIP .{P}" |
|
69 |
|
70 Ass "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" |
|
71 |
|
72 Local "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])} |
|
73 ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" |
|
74 |
|
75 Comp "[| G|-{P}.c.{Q}; |
|
76 G|-{Q}.d.{R} |] |
|
77 ==> G|-{P}. (c;;d) .{R}" |
|
78 |
|
79 If "[| G|-{P &> b }.c.{Q}; |
|
80 G|-{P &> (Not o b)}.d.{Q} |] |
|
81 ==> G|-{P}. IF b THEN c ELSE d .{Q}" |
|
82 |
|
83 Loop "G|-{P &> b}.c.{P} ==> |
|
84 G|-{P}. WHILE b DO c .{P &> (Not o b)}" |
|
85 |
|
86 (* |
|
87 BodyN "(insert ({P}. BODY pn .{Q}) G) |
|
88 |-{P}. the (body pn) .{Q} ==> |
|
89 G|-{P}. BODY pn .{Q}" |
|
90 *) |
|
91 Body "[| G Un (%p. {P p}. BODY p .{Q p})``Procs |
|
92 ||-(%p. {P p}. the (body p) .{Q p})``Procs |] |
|
93 ==> G||-(%p. {P p}. BODY p .{Q p})``Procs" |
|
94 |
|
95 Call "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} |
|
96 ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. |
|
97 X:=CALL pn(a) .{Q}" |
|
98 |
|
99 end |