Toy compiler
Compiles arithmetic experssions to a stack machine
Auteurs: Claude Marché
Catégories: Semantics of languages
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
theory Expr use int.Int type expr = Cte int | Plus expr expr | Minus expr expr | Mult expr expr function eval_expr (e:expr) : int = match e with | Cte n -> n | Plus e1 e2 -> eval_expr e1 + eval_expr e2 | Minus e1 e2 -> eval_expr e1 - eval_expr e2 | Mult e1 e2 -> eval_expr e1 * eval_expr e2 end end theory StackMachine type asm = Push int | Add | Sub | Mul use export int.Int use export list.List function compute (s:list int) (a:list asm) : list int = match a with | Nil -> s | Cons a r -> match a,s with | Push n, _ -> compute (Cons n s) r | Add, (Cons n1 (Cons n2 s)) -> compute (Cons (n2+n1) s) r | Sub, (Cons n1 (Cons n2 s)) -> compute (Cons (n2-n1) s) r | Mul, (Cons n1 (Cons n2 s)) -> compute (Cons (n2*n1) s) r | _ -> s end end end module Compiler use export list.Append use Expr use StackMachine function compile (e:expr) : list asm = match e with | Cte n -> Cons (Push n) Nil | Plus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Add Nil) | Minus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Sub Nil) | Mult e1 e2 -> compile e1 ++ (compile e2 ++ Cons Mul Nil) end let rec lemma soundness_gen (e:expr) (s:list int) (r:list asm) variant { e } ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r } = match e with | Cte n -> assert { compile e ++ r = Cons (Push n) r } | Plus e1 e2 -> soundness_gen e1 s (compile e2 ++ Cons Add r); soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r) | Minus e1 e2 -> soundness_gen e1 s (compile e2 ++ Cons Sub r); soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r) | Mult e1 e2 -> soundness_gen e1 s (compile e2 ++ Cons Mul r); soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r) end let lemma soundness (e:expr) ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) } = assert { compute Nil (compile e) = compute Nil (compile e ++ Nil) } end
download ZIP archive