sequential composition
state shorthands
represent pre-state, post-state by structures pre and post of sig State
c and c’ are short for pre :: c and post :: c
composition sugar
F ; G is short for some s : State | (let post be s | F) ? (let pre be s | G)
example
statements a = b.next ; c = a.next
formulas a’ = b.next ; c’ = a.next
desugar to :: (post :: a) = (pre :: b) . (pre :: next) ; (post :: c) = (pre :: a) . (pre :: next)
desugar ; some s : State | (s :: a) = (pre :: b) . (pre :: next) ? (post :: c) = (s :: a) . (s :: next)
resugar some s : State | (s :: a) = b.next ? c’ = (s :: a) . (s :: next)