Semester 2, 2018

# Tute (Week 6)

## 1 MinHS

Consider the code from last week's lecture. It contains a basic pretty printer and a type checker for our minimal MinHS.

Implement a Value type and an evaluator function for this language.

data Val = IntV Int | BoolV Bool | FunV (Expr -> Expr -> Expr)

eval :: Expr -> Val
eval (Num n) = IntV n
eval (Lit b) = BoolV b
eval (LessEq a b) = let
IntV x = eval a
IntV y = eval b
in BoolV (x <= y)
eval (Plus a b) = let
IntV x = eval a
IntV y = eval b
in IntV (x + y)
eval (If c t e) = let
BoolV b = eval c
in if b then eval t else eval e
eval (Recfun _ _ f) = FunV f
eval (Apply a b) = let
FunV f = eval a
arg    = eval b
in eval (f (uneval (FunV f)) (uneval arg))

uneval :: Val -> Expr
uneval (IntV v) = Num v
uneval (BoolV b) = Lit b
uneval (FunV f) = Recfun undefined undefined f

-- Use of undefined above is safe, as this is only used while
-- evaluating, where types are ignored anyway.


## 2 TinyImp

Suppose we wanted to extend TinyImp with a new type of loop:

$\mathbf{do}\ s\ \mathbf{until}\ e$

Which, running the loop body $$s$$ at least once, checks the guard of the loop after the loop body has executed, terminating if it is true (i.e. nonzero).

1. Give big-step semantics rules for this construct in the style of the lecture slides.
2. Propose a translation of this construct into existing TinyImp constructs.
3. Validate your translation by showing that the Hoare logic rule for this loop is derivable for your translation:

$\dfrac{ \{ \varphi \}\ s\ \{ \varphi \} }{\{ \varphi \}\ \mathbf{do}\ s\ \mathbf{until}\ e\ \{ \varphi \land e \} }$

1:

$\dfrac{ (\sigma_1, s) \Downarrow \sigma_2 \quad \sigma_2 \vdash e \Downarrow v \quad v \neq 0 }{ (\sigma_1, \mathbf{do}\ s\ \mathbf{until}\ e) \Downarrow \sigma_2 }$

$\dfrac{ (\sigma_1, s) \Downarrow \sigma_2 \quad \sigma_2 \vdash e \Downarrow 0 \quad (\sigma_2, \mathbf{do}\ s\ \mathbf{until}\ e) \Downarrow \sigma_3 }{ (\sigma_1, \mathbf{do}\ s\ \mathbf{until}\ e) \Downarrow \sigma_3 }$ 2:

$\mathbf{do}\ s\ \mathbf{until}\ e \equiv s; \mathbf{while}\ \neg e\ \mathbf{do}\ s\ \mathbf{od}$

3:

$\dfrac{ \dfrac{ }{\{ \varphi \}\ s\ \{ \varphi \}}\quad \dfrac{ \dfrac{ \dfrac{ \dfrac{}{\{ \varphi \}\ s\ \{ \varphi \} } }{ \{ \varphi \land \neg e \}\ s\ \{ \varphi \} }\text{Con} }{\{ \varphi \}\ \mathbf{while}\ \neg e\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land \neg (\neg e) \}}\text{Loop} }{\{ \varphi \}\ \mathbf{while}\ \neg e\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land e \}}\text{Con} }{\{ \varphi \}\ s; \mathbf{while}\ \neg e\ \mathbf{do}\ s\ \mathbf{od}\ \{ \varphi \land e \} }\text{Seq}$

## 3 Exam Questions

Your tutor will go through the big step semantics and proof questions from the midsession exam.

2018-11-16 Fri 19:37

Announcements RSS