Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/agda-hoare-satisfies.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 SemComm : Comm @$\rightarrow$@ Rel State (Level.zero) 1 SemComm : Comm !$\rightarrow$! Rel State (Level.zero)
2 SemComm Skip = RelOpState.deltaGlob 2 SemComm Skip = RelOpState.deltaGlob
3 SemComm Abort = RelOpState.emptyRel 3 SemComm Abort = RelOpState.emptyRel
4 SemComm (PComm pc) = PrimSemComm pc 4 SemComm (PComm pc) = PrimSemComm pc
5 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) 5 SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2)
6 SemComm (If b c1 c2) 6 SemComm (If b c1 c2)
9 (SemComm c1)) 9 (SemComm c1))
10 (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) 10 (RelOpState.comp (RelOpState.delta (NotP (SemCond b)))
11 (SemComm c2)) 11 (SemComm c2))
12 SemComm (While b c) 12 SemComm (While b c)
13 = RelOpState.unionInf 13 = RelOpState.unionInf
14 (@$\lambda$@ (n : $mathbb{N}$) @$\rightarrow$@ 14 (!$\lambda$! (n : $mathbb{N}$) !$\rightarrow$!
15 RelOpState.comp (RelOpState.repeat 15 RelOpState.comp (RelOpState.repeat
16 n 16 n
17 (RelOpState.comp 17 (RelOpState.comp
18 (RelOpState.delta (SemCond b)) 18 (RelOpState.delta (SemCond b))
19 (SemComm c))) 19 (SemComm c)))
20 (RelOpState.delta (NotP (SemCond b)))) 20 (RelOpState.delta (NotP (SemCond b))))
21 21
22 Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set 22 Satisfies : Cond !$\rightarrow$! Comm !$\rightarrow$! Cond !$\rightarrow$! Set
23 Satisfies bPre cm bPost 23 Satisfies bPre cm bPost
24 = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@ 24 = (s1 : State) !$\rightarrow$! (s2 : State) !$\rightarrow$!
25 SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2 25 SemCond bPre s1 !$\rightarrow$! SemComm cm s1 s2 !$\rightarrow$! SemCond bPost s2