Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/agda-hoare-rule.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 data HTProof : Cond -> Comm -> Cond -> Set where
2 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
3 (pr : Axiom bPre pcm bPost) ->
4 HTProof bPre (PComm pcm) bPost
5 SkipRule : (b : Cond) -> HTProof b Skip b
6 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
7 HTProof bPre Abort bPost
8 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
9 {bPost' : Cond} -> {bPost : Cond} ->
10 Tautology bPre bPre' ->
11 HTProof bPre' cm bPost' ->
12 Tautology bPost' bPost ->
13 HTProof bPre cm bPost
14 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
15 {cm2 : Comm} -> {bPost : Cond} ->
16 HTProof bPre cm1 bMid ->
17 HTProof bMid cm2 bPost ->
18 HTProof bPre (Seq cm1 cm2) bPost
19 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
20 {bPre : Cond} -> {bPost : Cond} ->
21 {b : Cond} ->
22 HTProof (bPre /\ b) cmThen bPost ->
23 HTProof (bPre /\ neg b) cmElse bPost ->
24 HTProof bPre (If b cmThen cmElse) bPost
25 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
26 HTProof (bInv /\ b) cm bInv ->
27 HTProof bInv (While b cm) (bInv /\ neg b)