Case Study: Interpreting an Imperative Language

{-@ measure useS @-} useS :: Stmt -> S.Set Var useS (Asgn x e) = useE e useS (If e s1 s2) = S.union (useE e) (S.union (useS s1) (useS s2)) useS (While e s) = S.union (useE e) (useS s) useS (Seq s1 s2) = S.union (useS s1) (S.difference (useS s2) (defS s1)) useS Skip = S.empty

{-@ measure defS @-} defS :: Stmt -> S.Set Var defS (Asgn x e) = S.singleton x defS (If e s1 s2) = S.intersection (defS s1) (defS s2) defS (While e s) = S.empty defS (Seq s1 s2) = S.union (defS s1) (defS s2) defS Skip = S.empty



Proving Something is Impossible



Calls to impossible only verify if they never occur at runtime.


{-@ impossible :: {v:String | false} -> a @-} impossible msg = error msg

Proving Something is Impossible



Exercise: What are valid inputs for safeDiv?


safeDiv :: Int -> Int -> Int safeDiv x y = if y == 0 then impossible "don't divide by zero!" else div x y

State

A datatype for mapping Var to their Value

data State = Emp -- ^ Empty `State` | Bind Var Val State -- ^ Extend `State` by assigning `Var` to `Val` -- | Update `s` by setting the value of `x` to `v` set :: Var -> Val -> State -> State set x v s = Bind x v s -- | Lookup the value of `x` in `s` get :: Var -> State -> Val get x (Bind y v s) | x == y = v -- ^ found the variable `x`, return v | otherwise = get x s -- ^ recursively search `s` get x Emp = impossible (x ++ " is undefined!")

Exercise: When is the last case in get indeed impossible?

Arithmetic Expressions


A datatype for representing arithmetic expressions

Sums of variables and integer constants

type Var = String type Val = Int data AExp = AVar Var -- ^ x | AVal Val -- ^ v | AAdd AExp AExp -- ^ e1 + e2

Evaluating Arithmetic Expressions


A recursive evaluator for Arithmetic Expressions

evalE :: State -> AExp -> Val evalE _ (AVal v) = v evalE st (AVar x) = get x st evalE st (AAdd e1 e2) = (evalE st e1) + (evalE st e2)

Exercise: How to verify the call to get is actually safe?

Variables Read in an Expression


Specify the Vars we need to get to evaluate an AExp

{-@ measure useE @-} useE :: AExp -> S.Set Var useE (AVar x) = S.empty -- TODO: replace with proper definition useE (AVal v) = S.empty -- TODO: replace with proper definition useE (AAdd e1 e2) = S.empty -- TODO: replace with proper definition {- | HINT : You may want to use * S.empty : the empty set * S.singleton x : the set containing just x * S.union s1 s2 : the union of s1 and s2 * S.intersection s1 s2 : the union of s1 and s2 * S.isSubsetOf s1 s2 : is s1 a subset of s2 ? -}

Exercise: Now, use useE to specify and verify evalE.

Statements


A datatype for representing imperative programs

Assignments, Sequencing, Branching and Loops.

data Stmt = Asgn Var AExp -- ^ x := e | If AExp Stmt Stmt -- ^ if (e != 0) {s1} else {s2} | While AExp Stmt -- ^ while (e != 0) {s} | Seq Stmt Stmt -- ^ s1; s2 | Skip -- ^ no-op

Evaluating Statements

A recursive interpreter for Statements

evalS :: State -> Stmt -> State evalS st Skip = st evalS st (Asgn x e) = set x (evalE st e) st evalS st (If e s1 s2) = if (evalE st e /= 0) then evalS st s1 else evalS st s2 evalS st w@(While e s) = if (evalE st e /= 0) then evalS st (Seq s w) else st evalS st (Seq s1 s2) = evalS (evalS st s1) s2

Exercise: When is it safe to call evalE st e?

Specify Used-Before-Defined Variables

Problem: Which Vars are used-before-definition in a Stmt?

{-@ measure useS @-} useS :: Stmt -> S.Set Var useS (Asgn x e) = S.empty -- TODO: replace with proper definition useS (If e s1 s2) = S.empty -- TODO: replace with proper definition useS (While e s) = S.empty -- TODO: replace with proper definition useS (Seq s1 s2) = S.empty -- TODO: replace with proper definition useS Skip = S.empty -- TODO: replace with proper definition {- | HINT: * S.empty : the empty set * S.singleton x : the set containing just x * S.union s1 s2 : the union of s1 and s2 * S.intersection s1 s2 : the union of s1 and s2 * S.isSubsetOf s1 s2 : is s1 a subset of s2 ? -}

Exercise: Now go back and specify and verify EvalS

Statically Verifying a Dynamic Check


interpret uses a run-time check to see if s is safe to evaluate.

interpret :: Stmt -> Maybe State interpret s | isSafe s = Just (evalS Emp s) | otherwise = Nothing {-@ inline isSafe @-} isSafe :: Stmt -> Bool isSafe s = True -- EXERCISE: replace with correct condition

Exercise: What run-time check isSafe statically ensures evalS Emp s won't crash?

Some Safe and Unsafe Programs

Here are some safe statements:

safe1 = (Asgn "X" (AVal 5)) `Seq` -- x := 5 (Asgn "Y" (AVar "X")) -- y := x safe2 = (If (AVal 1) -- if 1 (Asgn "Z" (AVal 1)) -- then z := 1 (Asgn "Z" (AVal 2)) -- else z := 2 ) `Seq` -- y = z (Asgn "Y" (AVar "Z"))

Here are some unsafe ones:

unsafe1 = (Asgn "X" (AVal 5)) `Seq` -- x := 5 (Asgn "Y" (AVar "Z")) -- y := z unsafe2 = (While (AVal 0) (Asgn "Z" (AVal 1))) `Seq` -- while (0) { z := 1} (Asgn "Y" (AVar "Z")) -- y := z