Mercurial > hg > Papers > 2020 > soto-midterm
view src/agda-hoare-satisfies.agda @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line source
SemComm : Comm -> 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 (λ (n : $mathbb{N}$) -> RelOpState.comp (RelOpState.repeat n (RelOpState.comp (RelOpState.delta (SemCond b)) (SemComm c))) (RelOpState.delta (NotP (SemCond b)))) Satisfies : Cond -> Comm -> Cond -> Set Satisfies bPre cm bPost = (s1 : State) -> (s2 : State) -> SemCond bPre s1 -> SemComm cm s1 s2 -> SemCond bPost s2