Mercurial > hg > Members > ryokka > HoareLogic

comparison HoareData.agda @ 22:e88ad1d70faf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate Hoare with whileTestPrim
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:24:54 +0900
parents whileTestPrim.agda@5e4abc1919b4
children
comparison
equal deleted inserted replaced
21:5e4abc1919b4 22:e88ad1d70faf
1 module HoareData
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
19 {-
20 prPre pr prPost
21 ------------- ------------------ ----------------
22 bPre => bPre' {bPre'} c {bPost'} bPost' => bPost
23 Weakening : ----------------------------------------------------
24 {bPre} c {bPost}
25
26 Assign: ----------------------------
27 {bPost[v<-e]} v:=e {bPost}
28
29 pr1 pr2
30 ----------------- ------------------
31 {bPre} cm1 {bMid} {bMid} cm2 {bPost}
32 Seq: ---------------------------------------
33 {bPre} cm1 ; cm2 {bPost}
34
35 pr1 pr2
36 ----------------------- ---------------------------
37 {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost}
38 If: ------------------------------------------------------
39 {bPre} If c then cm1 else cm2 fi {bPost}
40
41 pr
42 -------------------
43 {inv /\ c} cm {inv}
44 While: ---------------------------------------
45 {inv} while c do cm od {inv /\ neg c}
46 -}
47
48
49 data HTProof : Cond -> Comm -> Cond -> Set where
50 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
51 (pr : Axiom bPre pcm bPost) ->
52 HTProof bPre (PComm pcm) bPost
53 SkipRule : (b : Cond) -> HTProof b Skip b
54 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
55 HTProof bPre Abort bPost
56 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
57 {bPost' : Cond} -> {bPost : Cond} ->
58 Tautology bPre bPre' ->
59 HTProof bPre' cm bPost' ->
60 Tautology bPost' bPost ->
61 HTProof bPre cm bPost
62 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
63 {cm2 : Comm} -> {bPost : Cond} ->
64 HTProof bPre cm1 bMid ->
65 HTProof bMid cm2 bPost ->
66 HTProof bPre (Seq cm1 cm2) bPost
67 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
68 {bPre : Cond} -> {bPost : Cond} ->
69 {b : Cond} ->
70 HTProof (bPre and b) cmThen bPost ->
71 HTProof (bPre and neg b) cmElse bPost ->
72 HTProof bPre (If b cmThen cmElse) bPost
73 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
74 HTProof (bInv and b) cm bInv ->
75 HTProof bInv (While b cm) (bInv and neg b)
76