Sterling Example: modelingMSOS:bool

File: bool.sos

[Reduce File] [Raw File]

Module modelingMSOS:bool

Builds on modelingMSOS:host

e ::= ...
    | tt
    | ff

---------------------- [P-TT]
|{e}- tt ~~> intlit(1)

---------------------- [P-FF]
|{e}- ff ~~> intlit(0)



c ::= ...
    | ifte(e, c, c)
    | while(e, c)

---------------------------------------- [P-Ifte]
|{c}- ifte(Cond, Th, El) ~~> seq(Th, El)

-------------------------------- [P-While]
|{c}- while(Cond, Body) ~~> Body




ev Ctx C C1 Ctx1
------------------------------------------ [E-Ifte-Step]
ev_c Ctx ifte(C, T, E) ifte(C1, T, E) Ctx1


----------------------------- [E-Ifte-TT]
ev_c Ctx ifte(tt, T, E) T Ctx


----------------------------- [E-Ifte-FF]
ev_c Ctx ifte(ff, T, E) E Ctx


--------------------------------------------------------- [E-While]
{ev_c Ctx while(Cond, Body)
      ifte(Cond, seq(Body, while(Cond, Body)), nill) Ctx}




-------- [V-TT]
value tt

-------- [V-FF]
value ff