|
0
|
1 module Hoare
|
|
|
2 (PrimComm : Set)
|
|
|
3 (Cond : Set)
|
|
|
4 (Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set)
|
|
|
5 (Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set)
|
|
|
6 (_and_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond)
|
|
|
7 (neg : Cond @$\rightarrow$@ Cond )
|
|
|
8 where
|
|
|
9
|
|
|
10 data Comm : Set where
|
|
|
11 Skip : Comm
|
|
|
12 Abort : Comm
|
|
|
13 PComm : PrimComm @$\rightarrow$@ Comm
|
|
|
14 Seq : Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm
|
|
|
15 If : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm @$\rightarrow$@ Comm
|
|
|
16 While : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Comm
|
|
|
17
|
|
|
18 -- Hoare Triple
|
|
|
19 data HT : Set where
|
|
|
20 ht : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ HT
|
|
|
21
|
|
|
22 {-
|
|
|
23 prPre pr prPost
|
|
|
24 ------------- ------------------ ----------------
|
|
|
25 bPre => bPre' {bPre'} c {bPost'} bPost' => bPost
|
|
|
26 Weakening : ----------------------------------------------------
|
|
|
27 {bPre} c {bPost}
|
|
|
28
|
|
|
29 Assign: ----------------------------
|
|
|
30 {bPost[v<-e]} v:=e {bPost}
|
|
|
31
|
|
|
32 pr1 pr2
|
|
|
33 ----------------- ------------------
|
|
|
34 {bPre} cm1 {bMid} {bMid} cm2 {bPost}
|
|
|
35 Seq: ---------------------------------------
|
|
|
36 {bPre} cm1 ; cm2 {bPost}
|
|
|
37
|
|
|
38 pr1 pr2
|
|
|
39 ----------------------- ---------------------------
|
|
|
40 {bPre @$\wedge$@ c} cm1 {bPost} {bPre @$\wedge$@ neg c} cm2 {bPost}
|
|
|
41 If: ------------------------------------------------------
|
|
|
42 {bPre} If c then cm1 else cm2 fi {bPost}
|
|
|
43
|
|
|
44 pr
|
|
|
45 -------------------
|
|
|
46 {inv @$\wedge$@ c} cm {inv}
|
|
|
47 While: ---------------------------------------
|
|
|
48 {inv} while c do cm od {inv @$\wedge$@ neg c}
|
|
|
49 -}
|
|
|
50
|
|
|
51
|
|
|
52 data HTProof : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set where
|
|
|
53 PrimRule : {bPre : Cond} @$\rightarrow$@ {pcm : PrimComm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
54 (pr : Axiom bPre pcm bPost) @$\rightarrow$@
|
|
|
55 HTProof bPre (PComm pcm) bPost
|
|
|
56 SkipRule : (b : Cond) @$\rightarrow$@ HTProof b Skip b
|
|
|
57 AbortRule : (bPre : Cond) @$\rightarrow$@ (bPost : Cond) @$\rightarrow$@
|
|
|
58 HTProof bPre Abort bPost
|
|
|
59 WeakeningRule : {bPre : Cond} @$\rightarrow$@ {bPre' : Cond} @$\rightarrow$@ {cm : Comm} @$\rightarrow$@
|
|
|
60 {bPost' : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
61 Tautology bPre bPre' @$\rightarrow$@
|
|
|
62 HTProof bPre' cm bPost' @$\rightarrow$@
|
|
|
63 Tautology bPost' bPost @$\rightarrow$@
|
|
|
64 HTProof bPre cm bPost
|
|
|
65 SeqRule : {bPre : Cond} @$\rightarrow$@ {cm1 : Comm} @$\rightarrow$@ {bMid : Cond} @$\rightarrow$@
|
|
|
66 {cm2 : Comm} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
67 HTProof bPre cm1 bMid @$\rightarrow$@
|
|
|
68 HTProof bMid cm2 bPost @$\rightarrow$@
|
|
|
69 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
70 IfRule : {cmThen : Comm} @$\rightarrow$@ {cmElse : Comm} @$\rightarrow$@
|
|
|
71 {bPre : Cond} @$\rightarrow$@ {bPost : Cond} @$\rightarrow$@
|
|
|
72 {b : Cond} @$\rightarrow$@
|
|
|
73 HTProof (bPre and b) cmThen bPost @$\rightarrow$@
|
|
|
74 HTProof (bPre and neg b) cmElse bPost @$\rightarrow$@
|
|
|
75 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
76 WhileRule : {cm : Comm} @$\rightarrow$@ {bInv : Cond} @$\rightarrow$@ {b : Cond} @$\rightarrow$@
|
|
|
77 HTProof (bInv and b) cm bInv @$\rightarrow$@
|
|
|
78 HTProof bInv (While b cm) (bInv and neg b)
|
|
|
79
|
