Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/Hoare.agda @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
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