Wiki Agenda Contact Version française

Variations on Semantics of Programming Languages

This example provides solutions to exercises proposed by Olivier Danvy. It proposes several variations around different ways of defining the semantics of a language. It is presented in the paper Formalizing semantics with an automatic program verifier.


Authors: Claude Marché / Martin Clochard

Topics: Semantics of languages / Inductive predicates

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Defunctionalization

This is inspired from student exercises proposed by Olivier Danvy at the JFLA 2014 conference

Simple Arithmetic Expressions

module Expr

use export int.Int

Grammar of expressions

n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e

type expr = Cte int | Sub expr expr

type prog = expr

Examples:

p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)

let constant p0 : prog = Cte 0

let constant p1 : prog = Sub (Cte 10) (Cte 6)

let constant p2 : prog = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2))

let constant p3 : prog = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6))

let constant p4 : prog = Sub (Cte 10) (Sub (Cte 2) (Cte 3))

end

Direct Semantics

module DirectSem

use Expr

Values:

v  :  value
v ::= n
Expressible Values:
ve  :  expressible_value
ve ::= v
Interpretation:
------
n => n

e1 => n1   e2 => n2   n1 - n2 = n3
----------------------------------
      e1 - e2 => n3
A program e is interpreted into a value n if judgement
  e => n
holds.

Exercise 0.0

Program the interpreter above and test it on the examples.

  eval_0 : expression -> expressible_value
  interpret_0 : program -> expressible_value

(* Note: Why3 definitions introduced by "function" belong to the logic
   part of Why3 language *)

let rec function eval_0 (e:expr) : int =
  match e with
  | Cte n -> n
  | Sub e1 e2 -> eval_0 e1 - eval_0 e2
  end

let function interpret_0 (p:prog) : int = eval_0 p

Tests, can be replayed using

  why3 defunctionalization.mlw --exec DirectSem.test
(Why3 version at least 0.82 required)

let test () =
   interpret_0 p0,
   interpret_0 p1,
   interpret_0 p2,
   interpret_0 p3,
   interpret_0 p4

constant v3 : int = eval_0 p3

goal eval_p3 : v3 = 1

end

CPS: Continuation Passing Style

module CPS

use Expr

Exercise 0.1

CPS-transform (call by value, left to right) the function eval_0, and call it from the main interpreter with the identity function as initial continuation

      eval_1 : expression -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value

use DirectSem

let rec eval_1 (e:expr) (k: int->'a) : 'a
  variant { e }
  ensures { result = k (eval_0 e) }
= match e with
    | Cte n -> k n
    | Sub e1 e2 ->
      eval_1 e1 (fun v1 -> eval_1 e2 (fun v2 -> k (v1 - v2)))
  end

let interpret_1 (p : prog) : int
  ensures { result = eval_0 p }
= eval_1 p (fun n -> n)

end

Defunctionalization

module Defunctionalization

use Expr
use DirectSem

Exercise 0.2

De-functionalize the continuation of eval_1.

         cont ::= ...

   continue_2 : cont -> value -> value
       eval_2 : expression -> cont -> value
  interpret_2 : program -> value
The data type cont represents the grammar of contexts.

The two mutually recursive functions eval_2 and continue_2 implement an abstract machine, that is a state transition system.

type cont = A1 expr cont | A2 int cont | I

One would want to write in Why:

function eval_cont (c:cont) (v:int) : int =
  match c with
  | A1 e2 k ->
    let v2 = eval_0 e2 in
    eval_cont (A2 v k) v2
  | A2 v1 k -> eval_cont k (v1 - v)
  | I -> v
  end
But since the recursion is not structural, Why3 kernel rejects it (definitions in the logic part of the language must be total)

We replace that with a relational definition, an inductive one.

inductive eval_cont cont int int =
| a1 :
  forall e2:expr, k:cont, v:int, r:int.
  eval_cont (A2 v k) (eval_0 e2) r -> eval_cont (A1 e2 k) v r
| a2 :
  forall v1:int, k:cont, v:int, r:int.
  eval_cont k (v1 - v) r -> eval_cont (A2 v1 k) v r
| a3 :
  forall v:int. eval_cont I v v

Some functions to serve as measures for the termination proof

function size_e (e:expr) : int =
  match e with
  | Cte _ -> 1
  | Sub e1 e2 -> 3 + size_e e1 + size_e e2
  end

lemma size_e_pos: forall e: expr. size_e e >= 1

function size_c (c:cont) : int =
  match c with
  | I -> 0
  | A1 e2 k -> 2 + size_e e2 + size_c k
  | A2 _ k -> 1 + size_c k
  end

lemma size_c_pos: forall c: cont. size_c c >= 0

WhyML programs (declared with let instead of function), mutually recursive, resulting from de-functionalization

let rec continue_2 (c:cont) (v:int) : int
  variant { size_c c }
  ensures { eval_cont c v result }
  =
  match c with
    | A1 e2 k -> eval_2 e2 (A2 v k)
    | A2 v1 k -> continue_2 k (v1 - v)
    | I -> v
  end

with eval_2 (e:expr) (c:cont) : int
  variant { size_c c + size_e e }
  ensures { eval_cont c (eval_0 e) result }
  =
  match e with
    | Cte n -> continue_2 c n
    | Sub e1 e2 -> eval_2 e1 (A1 e2 c)
  end

The interpreter. The post-condition specifies that this program computes the same thing as eval_0

let interpret_2 (p:prog) : int
  ensures { result = eval_0 p }
  = eval_2 p I

let test () =
   interpret_2 p0,
   interpret_2 p1,
   interpret_2 p2,
   interpret_2 p3,
   interpret_2 p4

end

Defunctionalization with an algebraic variant

module Defunctionalization2

use Expr
use DirectSem

Exercise 0.2

De-functionalize the continuation of eval_1.

         cont ::= ...

   continue_2 : cont -> value -> value
       eval_2 : expression -> cont -> value
  interpret_2 : program -> value
The data type cont represents the grammar of contexts.

The two mutually recursive functions eval_2 and continue_2 implement an abstract machine, that is a state transition system.

type cont = A1 expr cont | A2 int cont | I

One would want to write in Why:

function eval_cont (c:cont) (v:int) : int =
  match c with
  | A1 e2 k ->
    let v2 = eval_0 e2 in
    eval_cont (A2 v k) v2
  | A2 v1 k -> eval_cont k (v1 - v)
  | I -> v
  end
But since the recursion is not structural, Why3 kernel rejects it (definitions in the logic part of the language must be total)

We replace that with a relational definition, an inductive one.

inductive eval_cont cont int int =
| a1 :
  forall e2:expr, k:cont, v:int, r:int.
  eval_cont (A2 v k) (eval_0 e2) r -> eval_cont (A1 e2 k) v r
| a2 :
  forall v1:int, k:cont, v:int, r:int.
  eval_cont k (v1 - v) r -> eval_cont (A2 v1 k) v r
| a3 :
  forall v:int. eval_cont I v v

Peano naturals to serve as the measure for the termination proof

type nat = S nat | O

function size_e (e:expr) (acc:nat) : nat =
  match e with
  | Cte _ -> S acc
  | Sub e1 e2 -> S (size_e e1 (S (size_e e2 (S acc))))
  end

function size_c (c:cont) (acc:nat) : nat =
  match c with
  | I -> acc
  | A1 e2 k -> S (size_e e2 (S (size_c k acc)))
  | A2 _ k -> S (size_c k acc)
  end

WhyML programs (declared with let instead of function), mutually recursive, resulting from de-functionalization

let rec continue_2 (c:cont) (v:int) : int
  variant { size_c c O }
  ensures { eval_cont c v result }
  =
  match c with
    | A1 e2 k -> eval_2 e2 (A2 v k)
    | A2 v1 k -> continue_2 k (v1 - v)
    | I -> v
  end

with eval_2 (e:expr) (c:cont) : int
  variant { size_e e (size_c c O) }
  ensures { eval_cont c (eval_0 e) result }
  =
  match e with
    | Cte n -> continue_2 c n
    | Sub e1 e2 -> eval_2 e1 (A1 e2 c)
  end

The interpreter. The post-condition specifies that this program computes the same thing as eval_0

let interpret_2 (p:prog) : int
  ensures { result = eval_0 p }
  = eval_2 p I

let test () =
   interpret_2 p0,
   interpret_2 p1,
   interpret_2 p2,
   interpret_2 p3,
   interpret_2 p4

end

Semantics with errors

module SemWithError

use Expr

Errors:

s  :  error
Expressible values:
ve  :  expressible_value
ve ::= v | s

type value = Vnum int | Underflow
(* in (Vnum n), n should always be >= 0 *)

Interpretation:

------
n => n

     e1 => s
------------
e1 - e2 => s

e1 => n1   e2 => s
------------------
      e1 - e2 => s

e1 => n1   e2 => n2   n1 < n2
-----------------------------
      e1 - e2 => "underflow"

e1 => n1   e2 => n2   n1 >= n2   n1 - n2 = n3
---------------------------------------------
      e1 - e2 => n3
We interpret the program e into value n if the judgement
  e => n
holds, and into error s if the judgement
  e => s
holds.

Exercise 1.0

Program the interpreter above and test it on the examples.

  eval_0 : expr -> expressible_value
  interpret_0 : program -> expressible_value

function eval_0 (e:expr) : value =
  match e with
  | Cte n -> if n >= 0 then Vnum n else Underflow
  | Sub e1 e2 ->
     match eval_0 e1 with
     | Underflow -> Underflow
     | Vnum v1 ->
       match eval_0 e2 with
       | Underflow -> Underflow
       | Vnum v2 ->
         if v1 >= v2 then Vnum (v1 - v2) else Underflow
       end
     end
  end

function interpret_0 (p:prog) : value = eval_0 p

Exercise 1.1

CPS-transform (call by value, from left to right) the function eval_0, call it from the main interpreter with the identity function as initial continuation.

      eval_1 : expr -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value

function eval_1 (e:expr) (k:value -> 'a) : 'a =
  match e with
    | Cte n -> k (if n >= 0 then Vnum n else Underflow)
    | Sub e1 e2 ->
      eval_1 e1 (fun v1 ->
       match v1 with
       | Underflow -> k Underflow
       | Vnum v1 ->
         eval_1 e2 (fun v2 ->
         match v2 with
         | Underflow -> k Underflow
         | Vnum v2 -> k (if v1 >= v2 then Vnum (v1 - v2) else Underflow)
         end)
       end)
  end

function interpret_1 (p : prog) : value = eval_1 p (fun n ->  n)

lemma cps_correct_expr:
  forall e: expr. forall k:value -> 'a. eval_1 e k = k (eval_0 e)

lemma cps_correct: forall p. interpret_1 p = interpret_0 p

Exercise 1.2

Divide the continuation

    expressible_value -> 'a
in two:
    (value -> 'a) * (error -> 'a)
and adapt eval_1 and interpret_1 as
       eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
  interpret_2 : program -> expressible_value

(*
function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
  match e with
    | Cte n -> if n >= 0 then k n else kerr ()
    | Sub e1 e2 ->
      eval_2 e1 (fun v1 ->
         eval_2 e2 (fun v2 ->
           if v1 >= v2 then k (v1 - v2) else kerr ())
           kerr) kerr
  end
*)

function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
  match e with
    | Cte n -> if n >= 0 then k n else kerr ()
    | Sub e1 e2 ->
      eval_2 e1 (eval_2a e2 k kerr) kerr
  end

with eval_2a (e2:expr) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
  (fun v1 ->  eval_2 e2 (eval_2b v1 k kerr) kerr)

with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
  (fun v2 ->  if v1 >= v2 then k (v1 - v2) else kerr ())

function interpret_2 (p : prog) : value =
  eval_2 p (fun n ->  Vnum n) (fun _ ->  Underflow)

lemma cps2_correct_expr_aux:
  forall k: int -> 'a, e1 e2, kerr: unit -> 'a.
  eval_2 (Sub e1 e2) k kerr = eval_2 e1 (eval_2a e2 k kerr) kerr

lemma cps2_correct_expr:
  forall e, kerr: unit->'a, k:int -> 'a. eval_2 e k kerr =
  match eval_0 e with Vnum n -> k n | Underflow -> kerr () end

lemma cps2_correct: forall p. interpret_2 p = interpret_0 p

Exercise 1.3

Specialize the codomain of the continuations and of the evaluation function so that it is not polymorphic anymore but is expressible_value, and then short-circuit the second continuation to stop in case of error

       eval_3 : expr -> (value -> expressible_value) -> expressible_value
  interpret_3 : program -> expressible_value
NB: Now there is only one continuation and it is applied only in absence of error.

function eval_3 (e:expr) (k:int -> value) : value =
  match e with
    | Cte n -> if n >= 0 then k n else Underflow
    | Sub e1 e2 ->
      eval_3 e1 (eval_3a e2 k)
  end

with eval_3a (e2:expr) (k:int -> value) : int -> value =
  (fun v1 ->  eval_3 e2 (eval_3b v1 k))

with eval_3b (v1:int) (k:int -> value) : int -> value =
  (fun v2 ->  if v1 >= v2 then k (v1 - v2) else Underflow)

function interpret_3 (p : prog) : value = eval_3 p (fun n ->  Vnum n)

let rec lemma cps3_correct_expr (e:expr) : unit
  variant { e }
  ensures { forall k. eval_3 e k =
    match eval_0 e with Vnum n -> k n | Underflow -> Underflow end }
= match e with
  | Cte _ -> ()
  | Sub e1 e2 ->
      cps3_correct_expr e1;
      cps3_correct_expr e2;
      assert {forall k. eval_3 e k = eval_3 e1 (eval_3a e2 k) }
  end

lemma cps3_correct: forall p. interpret_3 p = interpret_0 p

Exercise 1.4

De-functionalize the continuation of eval_3.

         cont ::= ...

    continue_4 : cont -> value -> expressible_value
        eval_4 : expr -> cont -> expressible_value
  interprete_4 : program -> expressible_value
The data type cont represents the grammar of contexts. (NB. has it changed w.r.t to previous exercise?)

The two mutually recursive functions eval_4 and continue_4 implement an abstract machine, that is a transition system that stops immediately in case of error, or and the end of computation.

type cont = I | A expr cont | B int cont

  end
</pre></blockquote>}
But since the recursion is not structural, Why3 kernel rejects it
(definitions in the logic part of the language must be total)

One would want to write in Why:

function eval_cont (c:cont) (v:value) : value =
  match v with
  | Underflow -> Underflow
  | Vnum v ->
  match c with
  | A e2 k -> eval_cont (B (Vnum v) k) (eval_0 e2)
  | B v1 k -> eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow)
  | I -> Vnum v (* v >= 0 by construction 

We replace that with a relational definition, an inductive one.

*)

inductive eval_cont cont value value =
| underflow :
  forall k:cont. eval_cont k Underflow Underflow
| a1 :
  forall e2:expr, k:cont, v:int, r:value.
  eval_cont (B v k) (eval_0 e2) r -> eval_cont (A e2 k) (Vnum v) r
| a2 :
  forall v1:int, k:cont, v:int, r:value.
  eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow) r
  -> eval_cont (B v1 k) (Vnum v) r
| a3 :
  forall v:int. eval_cont I (Vnum v) (Vnum v)

Some functions to serve as measures for the termination proof

function size_e (e:expr) : int =
  match e with
  | Cte _ -> 1
  | Sub e1 e2 -> 3 + size_e e1 + size_e e2
  end

lemma size_e_pos: forall e: expr. size_e e >= 1

use Defunctionalization as D

function size_c (c:cont) : int =
  match c with
  | I -> 0
  | A e2 k -> 2 + D.size_e e2 + size_c k
  | B _ k -> 1 + size_c k
  end

lemma size_c_pos: forall c: cont. size_c c >= 0

let rec continue_4 (c:cont) (v:int) : value
  requires { v >= 0 }
  variant { size_c c }
  ensures { eval_cont c (Vnum v) result }
  =
  match c with
    | A e2 k -> eval_4 e2 (B v k)
    | B v1 k -> if v1 >= v then continue_4 k (v1 - v) else Underflow
    | I -> Vnum v
  end

with eval_4 (e:expr) (c:cont) : value
  variant { size_c c + D.size_e e }
  ensures { eval_cont c (eval_0 e) result }
  =
  match e with
    | Cte n -> if n >= 0 then continue_4 c n else Underflow
    | Sub e1 e2 -> eval_4 e1 (A e2 c)
  end

The interpreter. The post-condition specifies that this program computes the same thing as eval_0

let interpret_4 (p:prog) : value
  ensures { result = eval_0 p }
  = eval_4 p I

let test () =
   interpret_4 p0,
   interpret_4 p1,
   interpret_4 p2,
   interpret_4 p3,
   interpret_4 p4

end

Reduction Semantics

module ReductionSemantics

A small step semantics, defined iteratively with reduction contexts

  use Expr
  use DirectSem

Expressions:

n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e

Values:

v  :  value
v ::= n

Potential Redexes:

  rp ::= n1 - n2

Reduction Rule:

  n1 - n2 -> n3
(in the case of relative integers Z, all potential redexes are true redexes; but for natural numbers, not all of them are true ones:
   n1 - n2 -> n3   if n1 >= n2
a potential redex that is not a true one is stuck.)

Contraction Function:

  contract : redex_potentiel -> expression + stuck
  contract (n1 - n2) = n3   si n3 = n1 - n2
and if there are only non-negative numbers:
  contract (n1 - n2) = n3     if n1 >= n2 and n3 = n1 - n2
  contract (n1 - n2) = stuck  if n1 < n2

predicate is_a_redex (e:expr) =
  match e with
  | Sub (Cte _) (Cte _) -> true
  | _ -> false
  end

let contract (e:expr) : expr
  requires { is_a_redex e }
  ensures { eval_0 result = eval_0 e }
  =
  match e with
  | Sub (Cte v1) (Cte v2) -> Cte (v1 - v2)
  | _ -> absurd
  end

Reduction Contexts:

C  : cont
C ::= [] | [C e] | [v C]

type context = Empty | Left context expr | Right int context

Recomposition:

             recompose : cont * expression -> expression
     recompose ([], e) = e
recompose ([C e2], e1) = recompose (C, e1 - e2)
recompose ([n1 C], e2) = recompose (C, n1 - e2)

let rec function recompose (c:context) (e:expr) : expr =
  match c with
  | Empty -> e
  | Left c e2 -> recompose c (Sub e e2)
  | Right n1 c -> recompose c (Sub (Cte n1) e)
  end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
  requires { eval_0 e1 = eval_0 e2 }
  variant  { c }
  ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
  | Empty -> ()
  | Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
  | Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
  end

(* not needed anymore
let rec lemma recompose_inversion (c:context) (e:expr)
  requires {
      match c with Empty -> false | _ -> true end \/
      match e with Cte _ -> false | Sub _ _ -> true end }
  variant { c }
  ensures {  match recompose c e with
               Cte _ -> false | Sub _ _ -> true end }
= match c with
  | Empty -> ()
  | Left c e2 -> recompose_inversion c (Sub e e2)
  | Right n1 c -> recompose_inversion c (Sub (Cte n1) e)
  end
*)

Decomposition:

dec_or_val = (C, rp) | v
Decomposition function:
             decompose_term : expression * cont -> dec_or_val
      decompose_term (n, C) = decompose_cont (C, n)
decompose_term (e1 - e2, C) = decompose_term (e1, [C e2])

             decompose_cont : cont * value -> dec_or_val
     decompose_cont ([], n) = n
  decompose_cont ([C e], n) = decompose_term (e, [n c])
decompose_term ([n1 C], n2) = (C, n1 - n2)

  decompose : expression -> dec_or_val
decompose e = decompose_term (e, [])

exception Stuck

predicate is_a_value (e:expr) =
  match e with
  | Cte _ -> true
  | _ -> false
  end

predicate is_empty_context (c:context) =
  match c with
  | Empty -> true
  | _ -> false
  end

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
  match c with
  | Empty -> 0
  | Left c e -> 2 + size_c c + size_e e
  | Right _ c -> 1 + size_c c
  end

lemma size_c_pos: forall c: context. size_c c >= 0

let rec decompose_term (e:expr) (c:context) : (context, expr)
  variant { size_e e + size_c c }
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c e /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c /\ is_a_value e }
  (* raises { Stuck -> is_a_value (recompose c e) } *)
  =
  match e with
  | Cte n -> decompose_cont c n
  | Sub e1 e2 -> decompose_term e1 (Left c e2)
  end

with decompose_cont (c:context) (n:int) : (context, expr)
  variant { size_c c }
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c (Cte n)  /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c }
(*  raises { Stuck -> is_a_value (recompose c (Cte n)) } *)
  =
  match c with
  | Empty -> raise Stuck
  | Left c e -> decompose_term e (Right n c)
  | Right n1 c -> c, Sub (Cte n1) (Cte n)
  end

let decompose (e:expr) : (context, expr)
  ensures { let c1,e1 = result in recompose c1 e1 = e  /\
            is_a_redex e1 }
  raises { Stuck -> is_a_value e }
  =
  decompose_term e Empty

One reduction step:

reduce : expression -> expression + stuck

if decompose e = v
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = stuck
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = c
then reduce e = recompose (C, c)

Exercise 2.0

Implement the reduction semantics above and test it

let reduce (e:expr) : expr
  ensures { eval_0 result = eval_0 e }
  raises { Stuck -> is_a_value e }
  =
  let c,r = decompose e in
  recompose c (contract r)

Evaluation based on iterated reduction:

itere : red_ou_val -> value + erreur

itere v = v

if contract rp = stuck
then itere (C, rp) = stuck

if contract rp = c
then itere (C, rp) = itere (decompose (recompose (C, c)))

let rec itere (e:expr) : int
  diverges (* termination could be proved but that's not the point *)
  ensures { eval_0 e = result }
  =
  match reduce e with
  | e' -> itere e'
  | exception Stuck ->
     match e with
     | Cte n -> n
     | _ -> absurd
     end
  end

Exercise 2.1

Optimize the step recomposition / decomposition into a single function refocus.

let refocus c e
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c e /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c /\ is_a_value e }
= decompose_term e c

let rec itere_opt (c:context) (e:expr) : int
  diverges
  ensures { result = eval_0 (recompose c e) }
= match refocus c e with
  | c, r -> itere_opt c (contract r)
  | exception Stuck ->
     assert { is_empty_context c };
     match e with
     | Cte n -> n
     | _ -> absurd
     end
  end

let rec normalize (e:expr)
  diverges
  ensures { result = eval_0 e }
= itere_opt Empty e

Exercise 2.2

Derive an abstract machine

(c,Cte n)_1 -> (c,n)_2
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop with result = n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1

let rec eval_1 c e
  variant { 2 * (size_c c + size_e e) }
  ensures { result = eval_0 (recompose c e) }
= match e with
  | Cte n -> eval_2 c n
  | Sub e1 e2 -> eval_1 (Left c e2) e1
  end

with eval_2 c n
  variant { 1 + 2 * size_c c }
  ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
  | Empty -> n
  | Left c e -> eval_1 (Right n c) e
  | Right n1 c -> eval_1 c (Cte (n1 - n))
  end

let interpret p
  ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
   interpret p0,
   interpret p1,
   interpret p2,
   interpret p3,
   interpret p4

end

module RWithError

use Expr
use SemWithError

Exercise 2.3

An abstract machine for the case with errors

(c,Cte n)_1 -> stop on Underflow if  n < 0
(c,Cte n)_1 -> (c,n)_2 if n >= 0
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop on Vnum n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> stop on Underflow if n1 < n
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1 if n1 >= n

type context = Empty | Left context expr | Right int context

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
  match c with
  | Empty -> 0
  | Left c e -> 2 + size_c c + size_e e
  | Right _ c -> 1 + size_c c
  end

lemma size_c_pos: forall c: context. size_c c >= 0

function recompose (c:context) (e:expr) : expr =
  match c with
  | Empty -> e
  | Left c e2 -> recompose c (Sub e e2)
  | Right n1 c -> recompose c (Sub (Cte n1) e)
  end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
  requires { eval_0 e1 = eval_0 e2 }
  variant  { c }
  ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
  | Empty -> ()
  | Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
  | Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
  end

let rec lemma recompose_underflow (c:context) (e:expr) : unit
  requires { eval_0 e = Underflow }
  variant { c }
  ensures { eval_0 (recompose c e) = Underflow }
= match c with
  | Empty -> ()
  | Left c e1 -> recompose_underflow c (Sub e e1)
  | Right n c -> recompose_underflow c (Sub (Cte n) e)
  end

let rec eval_1 c e
  variant { 2 * (size_c c + size_e e) }
  ensures { result = eval_0 (recompose c e) }
= match e with
  | Cte n -> if n >= 0 then eval_2 c n else Underflow
  | Sub e1 e2 -> eval_1 (Left c e2) e1
  end

with eval_2 c n
  variant { 1 + 2 * size_c c }
  requires { n >= 0 }
  ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
  | Empty -> Vnum n
  | Left c e -> eval_1 (Right n c) e
  | Right n1 c -> if n1 >= n then eval_1 c (Cte (n1 - n)) else Underflow
  end

let interpret p
  ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
   interpret p0,
   interpret p1,
   interpret p2,
   interpret p3,
   interpret p4

end

download ZIP archive