1
|
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
|