wp2.mlw

(** {1 A certified WP calculus} *)

(** {2 A simple imperative language, syntax and semantics} *)

theory Imp

(** terms and formulas *)

type datatype = Tint | Tbool

type operator = Oplus | Ominus | Omult | Ole

type ident = int

type term =
  | Tconst int
  | Tvar ident
  | Tderef ident
  | Tbin term operator term

type fmla =
  | Fterm term
  | Fand fmla fmla
  | Fnot fmla
  | Fimplies fmla fmla
  | Flet ident term fmla
  | Fforall ident datatype fmla

use import int.Int
use import bool.Bool

type value =
  | Vint int
  | Vbool bool

use map.Map as IdMap
type env = IdMap.map ident value

(** semantics of formulas *)

function eval_bin (x:value) (op:operator) (y:value) : value =
  match x,y with
  | Vint x,Vint y ->
     match op with
     | Oplus -> Vint (x+y)
     | Ominus -> Vint (x-y)
     | Omult -> Vint (x*y)
     | Ole -> Vbool (if x <= y then True else False)
     end
  | _,_ -> Vbool False
  end

function get_env (i:ident) (e:env) : value = IdMap.get e i

function eval_term (sigma:env) (pi:env) (t:term) : value =
  match t with
  | Tconst n -> Vint n
  | Tvar id -> get_env id pi
  | Tderef id -> get_env id sigma
  | Tbin t1 op t2 ->
     eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
  end

predicate eval_fmla (sigma:env) (pi:env) (f:fmla) =
  match f with
  | Fterm t -> eval_term sigma pi t = Vbool True
  | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
  | Fnot f -> not (eval_fmla sigma pi f)
  | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2