Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/agda-hoare-satisfies.agda.replaced @ 4:b5fffa8ae875
fix chapter hoare
author | ryokka |
---|---|
date | Wed, 29 Jan 2020 22:36:17 +0900 |
parents | |
children |
line wrap: on
line source
SemComm : Comm @$\rightarrow$@ Rel State (Level.zero) SemComm Skip = RelOpState.deltaGlob SemComm Abort = RelOpState.emptyRel SemComm (PComm pc) = PrimSemComm pc SemComm (Seq c1 c2) = RelOpState.comp (SemComm c1) (SemComm c2) SemComm (If b c1 c2) = RelOpState.union (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c1)) (RelOpState.comp (RelOpState.delta (NotP (SemCond b))) (SemComm c2)) SemComm (While b c) = RelOpState.unionInf (@$\lambda$@ (n : $mathbb{N}$) @$\rightarrow$@ RelOpState.comp (RelOpState.repeat n (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c))) (RelOpState.delta (NotP (SemCond b)))) Satisfies : Cond @$\rightarrow$@ Comm @$\rightarrow$@ Cond @$\rightarrow$@ Set Satisfies bPre cm bPost = (s1 : State) @$\rightarrow$@ (s2 : State) @$\rightarrow$@ SemCond bPre s1 @$\rightarrow$@ SemComm cm s1 s2 @$\rightarrow$@ SemCond bPost s2