•kind
State = Open | Closed
•
•data
V s t
• = forall st . Z where s =
(t,st)
• | forall st t1 . S (V st t)
• where s =
(t1,st)
•
•
•data
Com st x y
• = forall t . Set (V st t) (Exp st t) where
x=y
• | forall a . Seq (Com st x a) (Com st a y)
• | If (Exp st Bool) (Com st x y) (Com st x
y)
• | While (Exp st Bool) (Com st x y) where x =
y
• | forall t . Declare (Exp st t) (Com (t,st)
x y)
• | Open where x = Closed, y = Open
• | Close where x = Open, y = Closed
• | Write (Exp st Int) where x = Open, y = Open
•