|
1
|
1 module Hoare
|
|
|
2 (PrimComm : Set)
|
|
|
3 (Cond : Set)
|
|
|
4 (Axiom : Cond -> PrimComm -> Cond -> Set)
|
|
|
5 (Tautology : Cond -> Cond -> Set)
|
|
|
6 (_and_ : Cond -> Cond -> Cond)
|
|
|
7 (neg : Cond -> Cond )
|
|
|
8 where
|
|
|
9
|
|
|
10 data Comm : Set where
|
|
|
11 Skip : Comm
|
|
|
12 Abort : Comm
|
|
|
13 PComm : PrimComm -> Comm
|
|
|
14 Seq : Comm -> Comm -> Comm
|
|
|
15 If : Cond -> Comm -> Comm -> Comm
|
|
|
16 While : Cond -> Comm -> Comm
|
|
|
17
|
|
|
18 -- Hoare Triple
|
|
|
19 data HT : Set where
|
|
|
20 ht : Cond -> Comm -> Cond -> 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 /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost}
|
|
|
41 If: ------------------------------------------------------
|
|
|
42 {bPre} If c then cm1 else cm2 fi {bPost}
|
|
|
43
|
|
|
44 pr
|
|
|
45 -------------------
|
|
|
46 {inv /\ c} cm {inv}
|
|
|
47 While: ---------------------------------------
|
|
|
48 {inv} while c do cm od {inv /\ neg c}
|
|
|
49 -}
|
|
|
50
|
|
|
51
|
|
|
52 data HTProof : Cond -> Comm -> Cond -> Set where
|
|
|
53 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
|
|
|
54 (pr : Axiom bPre pcm bPost) ->
|
|
|
55 HTProof bPre (PComm pcm) bPost
|
|
|
56 SkipRule : (b : Cond) -> HTProof b Skip b
|
|
|
57 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
|
|
|
58 HTProof bPre Abort bPost
|
|
|
59 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
|
|
|
60 {bPost' : Cond} -> {bPost : Cond} ->
|
|
|
61 Tautology bPre bPre' ->
|
|
|
62 HTProof bPre' cm bPost' ->
|
|
|
63 Tautology bPost' bPost ->
|
|
|
64 HTProof bPre cm bPost
|
|
|
65 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
|
|
|
66 {cm2 : Comm} -> {bPost : Cond} ->
|
|
|
67 HTProof bPre cm1 bMid ->
|
|
|
68 HTProof bMid cm2 bPost ->
|
|
|
69 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
70 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
|
|
|
71 {bPre : Cond} -> {bPost : Cond} ->
|
|
|
72 {b : Cond} ->
|
|
|
73 HTProof (bPre and b) cmThen bPost ->
|
|
|
74 HTProof (bPre and neg b) cmElse bPost ->
|
|
|
75 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
76 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
|
|
|
77 HTProof (bInv and b) cm bInv ->
|
|
|
78 HTProof bInv (While b cm) (bInv and neg b)
|
|
|
79
|
