Mercurial > hg > Members > ryokka > HoareLogic

annotate Hoare.agda @ 52:0bde332e1215

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use state as t
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 19 Dec 2019 15:48:11 +0900
parents e668962ac31a
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
24
e668962ac31a rename modules
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
1 module Hoare
22
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
2 (PrimComm : Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
3 (Cond : Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
4 (Axiom : Cond -> PrimComm -> Cond -> Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
5 (Tautology : Cond -> Cond -> Set)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
6 (_and_ : Cond -> Cond -> Cond)
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
7 (neg : Cond -> Cond )
e88ad1d70faf separate Hoare with whileTestPrim
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
8 where
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 data Comm : Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 Skip : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 Abort : Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 PComm : PrimComm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 Seq : Comm -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 If : Cond -> Comm -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 While : Cond -> Comm -> Comm
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
18
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
19 {-
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
20 prPre pr prPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
21 ------------- ------------------ ----------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
22 bPre => bPre' {bPre'} c {bPost'} bPost' => bPost
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
23 Weakening : ----------------------------------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
24 {bPre} c {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
26 Assign: ----------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
27 {bPost[v<-e]} v:=e {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
28
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
29 pr1 pr2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
30 ----------------- ------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
31 {bPre} cm1 {bMid} {bMid} cm2 {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
32 Seq: ---------------------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
33 {bPre} cm1 ; cm2 {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
34
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
35 pr1 pr2
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
36 ----------------------- ---------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
37 {bPre /\ c} cm1 {bPost} {bPre /\ neg c} cm2 {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
38 If: ------------------------------------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
39 {bPre} If c then cm1 else cm2 fi {bPost}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
40
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
41 pr
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
42 -------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
43 {inv /\ c} cm {inv}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
44 While: ---------------------------------------
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
45 {inv} while c do cm od {inv /\ neg c}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
46 -}
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
47
6417f6d821e6 add Hoare again
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
48
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 data HTProof : Cond -> Comm -> Cond -> Set where
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 (pr : Axiom bPre pcm bPost) ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 HTProof bPre (PComm pcm) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 SkipRule : (b : Cond) -> HTProof b Skip b
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 HTProof bPre Abort bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 {bPost' : Cond} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 Tautology bPre bPre' ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 HTProof bPre' cm bPost' ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 Tautology bPost' bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 HTProof bPre cm bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 {cm2 : Comm} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 HTProof bPre cm1 bMid ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 HTProof bMid cm2 bPost ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 HTProof bPre (Seq cm1 cm2) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 {bPre : Cond} -> {bPost : Cond} ->
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 {b : Cond} ->
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
70 HTProof (bPre and b) cmThen bPost ->
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
71 HTProof (bPre and neg b) cmElse bPost ->
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 HTProof bPre (If b cmThen cmElse) bPost
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
10
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
74 HTProof (bInv and b) cm bInv ->
bc819bdda374 proof completed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
75 HTProof bInv (While b cm) (bInv and neg b)
3
6be8ee856666 add simple Hoare logic example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76