COMP[39]161 Concepts of Programming Languages
Semester 2, 2018

Tute (Week 6)

Table of Contents

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 \} } \]


\[ \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}\]


\[ \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