Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/agda-hoare-satisfies.agda.replaced @ 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 SemComm : Comm @$\rightarrow$@ Rel State (Level.zero)
2 SemComm Skip = RelOpState.deltaGlob
3 SemComm Abort = RelOpState.emptyRel
4 SemComm (PComm pc) = PrimSemComm pc
5 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
6 SemComm (If b c1 c2)
7 = RelOpState.union
8 (RelOpState.comp (RelOpState.delta (SemCond b))
9 (SemComm c1))
10 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
11 (SemComm c2))
12 SemComm (While b c)
13 = RelOpState.unionInf
14 (@$\lambda$@ (n : $mathbb{N}$) @$\rightarrow$@
15 RelOpState.comp (RelOpState.repeat
16 n
17 (RelOpState.comp
18 (RelOpState.delta (SemCond b))
19 (SemComm c)))
20 (RelOpState.delta (NotP (SemCond b))))
21
22 Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set
23 Satisfies bPre cm bPost
24 = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@
25 SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2