various examples from Rustan's book

parent 7d23cdff
(** Various examples from the book "Program Proofs" by Rustan Leino *)
module Mult
use int.Int
let rec function mult (x y: int) : int
requires { y >= 0 }
variant { y }
= if y = 0 then 0 else x + mult x (y - 1)
let rec lemma mult_commutative (x y: int)
requires { x >= 0 }
requires { y >= 0 }
variant { x, y }
ensures { mult x y = mult y x }
= if x = y then
else if x = 0 then
mult_commutative x (y-1)
else if y < x then
mult_commutative y x
else begin
mult_commutative x (y-1);
mult_commutative (x-1) (y-1);
mult_commutative (x-1) y
module Mirror
use bintree.Tree
let rec function mirror (t: tree 'a) : tree 'a
variant { t }
= match t with
| Empty -> Empty
| Node l x r -> Node (mirror r) x (mirror l) end
let rec lemma mirror_involutive (t: tree 'a)
variant { t }
ensures { mirror (mirror t) = t }
= match t with
| Empty -> () | Node l _ r -> mirror_involutive l; mirror_involutive r end
use bintree.Size
let rec lemma mirror_size (t: tree 'a)
variant { t }
ensures { size (mirror t) = size t }
= match t with
| Empty -> () | Node l _ r -> mirror_size l; mirror_size r end
module AST
use int.Int
use list.List
use string.OCaml
type op = Add | Mul
type expr =
| Const int
| Var string
| Node op (list expr)
clone fmap.MapApp with type key = string, val eq = OCaml.(=)
type env = t int
let function unit (op: op) : int
= match op with Add -> 0 | Mul -> 1 end
let rec function eval (e: expr) (env: env) : int
variant { e }
= match e with
| Const n -> n
| Var s -> if mem s env then find s env else 0
| Node op args -> eval_list op args env
with function eval_list (op: op) (args: list expr) (env: env) : int
variant { args }
= match args with
| Nil -> unit op
| Cons e l ->
let v0 = eval e env in
let v1 = eval_list op l env in
match op with
| Add -> v0 + v1
| Mul -> v0 * v1
(* Instead of lemmas shorten_correct, optimize_correct, etc.
we give suitable postconditions to the various functions.
Note that, despite these postconditions, the functions are still
available in the logic (because they are declared with the
'function' keyword). The postconditions are also turned into
lemmas about these functions. *)
let function shorten (op: op) (args: list expr) : expr
ensures { forall env. eval result env = eval (Node op args) env }
= match args with
| Nil -> Const (unit op)
| Cons e Nil -> e
| _ -> Node op args
let rec function optimize (e: expr) : expr
variant { e }
ensures { forall env. eval result env = eval e env }
= match e with
| Const _
| Var _ -> e
| Node op args -> shorten op (optimize_and_filter args (unit op))
with function optimize_and_filter (args: list expr) (u: int) : list expr
variant { args }
ensures { forall op env. u = unit op ->
eval (Node op result) env = eval (Node op args) env }
= match args with
| Nil -> Nil
| Cons e l ->
let e = optimize e in
let l = optimize_and_filter l u in
match e with Const n -> if n = u then l else Cons e l | _ -> Cons e l end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.7" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="program_proofs.mlw"/>
<theory name="Mult" proved="true">
<goal name="mult&#39;vc" expl="VC for mult" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
<goal name="mult_commutative&#39;vc" expl="VC for mult_commutative" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
<theory name="Mirror" proved="true">
<goal name="mirror&#39;vc" expl="VC for mirror" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="41"/></proof>
<goal name="mirror_involutive&#39;vc" expl="VC for mirror_involutive" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
<goal name="mirror_size&#39;vc" expl="VC for mirror_size" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="135"/></proof>
<theory name="AST" proved="true">
<goal name="MapApp.eq&#39;refn&#39;vc" expl="VC for eq&#39;refn" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="10"/></proof>
<goal name="eval&#39;vc" expl="VC for eval" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="78"/></proof>
<goal name="eval_list&#39;vc" expl="VC for eval_list" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="69"/></proof>
<goal name="shorten&#39;vc" expl="VC for shorten" proved="true">
<proof prover="1"><result status="valid" time="0.20" steps="35469"/></proof>
<goal name="optimize&#39;vc" expl="VC for optimize" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="148"/></proof>
<goal name="optimize_and_filter&#39;vc" expl="VC for optimize_and_filter" proved="true">
<proof prover="1"><result status="valid" time="0.50" steps="95446"/></proof>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment