Skip to content

why3
why3
Commit 1b644c8e authored by Mário Pereira's avatar Mário Pereira
Browse files
Options

Code extraction (wip)

parent 3172196f
Hide whitespace changes
Inline Side-by-side
Showing with 235 additions and 267 deletions
examples/leftist_heap.mlw
View file @ 1b644c8e
......@@ -141,8 +141,8 @@ module LeftistHeap
= match h with
| E -> absurd
| N _ l _ r ->
match l with E -> root_is_miminum l | _ -> () end;
match r with E -> root_is_miminum r | _ -> () end
match l with E -> () | _ -> root_is_miminum l end;
match r with E -> () | _ -> root_is_miminum r end
end
function rank (h: t) : int = match h with
......
examples/leftist_heap/why3session.xml
View file @ 1b644c8e
......@@ -3,140 +3,107 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../leftist_heap.mlw" expanded="true">
<theory name="Heap" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../leftist_heap.mlw">
<theory name="Heap" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TreeRank" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="TreeRank" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Size" sum="6f414cd8c85262f7a883e226a4add0bb">
<theory name="Size" sum="258605247b400f25a721b00c9b435e68">
<goal name="VC size" expl="VC for size">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="size_nonneg">
<transf name="induction_ty_lex">
<goal name="size_nonneg.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="size_empty">
<transf name="induction_ty_lex">
<goal name="size_empty.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Occ" sum="86544f99c8754e786af5d51f9f25891d" expanded="true">
<goal name="occ_nonneg" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<theory name="Occ" sum="999685546cd28de26822da69eae52f80">
<goal name="occ_nonneg">
<transf name="induction_ty_lex">
<goal name="occ_nonneg.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LeftistHeap" sum="58ee1098b455dc82539ced85085de45b" expanded="true">
<goal name="le_root_trans">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
<theory name="LeftistHeap" sum="b38f2f0e033563cc31244689f92a6c65">
<goal name="VC le_root" expl="VC for le_root">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="WP_parameter root_is_miminum" expl="VC for root_is_miminum" expanded="true">
<proof prover="0"><result status="valid" time="0.13"/></proof>
<goal name="le_root_trans">
<proof prover="2"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC root_is_miminum" expl="VC for root_is_miminum">
<proof prover="2"><result status="valid" time="0.77" steps="1597"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC empty" expl="VC for empty">
<proof prover="2"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
<goal name="VC is_empty" expl="VC for is_empty">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter rank" expl="VC for rank">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
<goal name="VC rank" expl="VC for rank">
<proof prover="2"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
<goal name="WP_parameter make_n" expl="VC for make_n">
<proof prover="1"><result status="valid" time="0.21" steps="819"/></proof>
<goal name="VC make_n" expl="VC for make_n">
<proof prover="2"><result status="valid" time="0.06" steps="239"/></proof>
</goal>
<goal name="WP_parameter merge" expl="VC for merge">
<goal name="VC merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.10" expl="10. variant decrease">
<proof prover="1"><result status="valid" time="0.03" steps="65"/></proof>
</goal>
<goal name="WP_parameter merge.11" expl="11. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter merge.12" expl="12. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter merge.13" expl="13. precondition">
<proof prover="0"><result status="valid" time="0.26"/></proof>
<goal name="VC merge.1" expl="1. variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter merge.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="29"/></proof>
<goal name="VC merge.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="91"/></proof>
</goal>
<goal name="WP_parameter merge.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="46"/></proof>
<goal name="VC merge.3" expl="3. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="104"/></proof>
</goal>
<goal name="WP_parameter merge.16" expl="16. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
<goal name="VC merge.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter merge.17" expl="17. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="66"/></proof>
<goal name="VC merge.5" expl="5. variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="WP_parameter merge.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
<goal name="VC merge.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="92"/></proof>
</goal>
<goal name="WP_parameter merge.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
<goal name="VC merge.7" expl="7. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="105"/></proof>
</goal>
<goal name="WP_parameter merge.20" expl="20. precondition">
<proof prover="0"><result status="valid" time="0.64"/></proof>
<goal name="VC merge.8" expl="8. precondition">
<proof prover="0"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter merge.21" expl="21. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
<goal name="VC merge.9" expl="9. postcondition">
<proof prover="2"><result status="valid" time="0.05" steps="214"/></proof>
</goal>
<goal name="WP_parameter merge.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
<goal name="VC merge.10" expl="10. postcondition">
<proof prover="2"><result status="valid" time="0.13" steps="385"/></proof>
</goal>
<goal name="WP_parameter merge.23" expl="23. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
<goal name="VC merge.11" expl="11. postcondition">
<proof prover="2"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insert" expl="VC for insert">
<proof prover="1"><result status="valid" time="0.04" steps="124"/></proof>
<goal name="VC insert" expl="VC for insert">
<proof prover="2"><result status="valid" time="0.05" steps="146"/></proof>
</goal>
<goal name="WP_parameter find_min" expl="VC for find_min">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
<goal name="VC find_min" expl="VC for find_min">
<proof prover="2"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter delete_min" expl="VC for delete_min">
<proof prover="1"><result status="valid" time="0.03" steps="126"/></proof>
<goal name="VC delete_min" expl="VC for delete_min">
<proof prover="2"><result status="valid" time="0.04" steps="220"/></proof>
</goal>
</theory>
</file>
......
modules/mach/int.mlw
View file @ 1b644c8e
......@@ -49,30 +49,30 @@ module Bounded_int
predicate in_bounds (n:int) = min <= n <= max
axiom to_int_in_bounds: forall n:t. in_bounds (to_int n)
axiom to_int_in_bounds: forall n:t. in_bounds n
val of_int (n:int) : t
requires { "expl:integer overflow" in_bounds n }
ensures { to_int result = n }
ensures { result = n }
val (+) (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a + to_int b) }
ensures { to_int result = to_int a + to_int b }
requires { "expl:integer overflow" in_bounds (a + b) }
ensures { result = a + b }
val (-) (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a - to_int b) }
ensures { to_int result = to_int a - to_int b }
requires { "expl:integer overflow" in_bounds (a - b) }
ensures { result = a - b }
val (*) (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (to_int a * to_int b) }
ensures { to_int result = to_int a * to_int b }
val ( * ) (a:t) (b:t) : t
requires { "expl:integer overflow" in_bounds (a * b) }
ensures { result = a * b }
val (-_) (a:t) : t
requires { "expl:integer overflow" in_bounds (- to_int a) }
ensures { to_int result = - to_int a }
requires { "expl:integer overflow" in_bounds (- a) }
ensures { result = - a }
val eq (a:t) (b:t) : bool
ensures { to_int a = to_int b -> result }
ensures { to_int a = to_int b -> result } (* leave this to_int ? *)
ensures { result -> a = b }
val ne (a:t) (b:t) : bool
......
modules/ocaml.mlw
View file @ 1b644c8e
(* module OCaml *)
module OCaml
(* use export int.Int *)
(* use export int.MinMax *)
(* use export option.Option *)
(* use export list.List *)
(* use export seq.Seq *)
use export int.Int
use export int.MinMax
use export option.Option
use export list.List
use export seq.Seq
(* scope Sys *)
(* constant max_array_length : int *)
(* end *)
scope Sys
constant max_array_length : int
end
(* use array.Array *)
(* type array 'a = Array.array 'a *)
use array.Array
type array 'a = Array.array 'a
(* end *)
end
module Sys
......
tests/test_extraction_mario.mlw
View file @ 1b644c8e
module M
use import mach.int.Int31
use import mach.int.Int63
let f (x: int31) : int
= min_int31
let f (x: int63) : int
= min_int63
(* use import seq.Seq *)
use import seq.Seq
use import int.Int
(* let function f (y: int) (x: int) : int *)
(* requires { x >= 0 } *)
(* ensures { result >= 0 } *)
(* = x *)
let function f_function (y: int) (x: int) : int
requires { x >= 0 }
ensures { result >= 0 }
= x
(* let g (ghost z: int) (x: int) : int *)
(* requires { x > 0 } *)
(* ensures { result > 0 } *)
(* = let y = x in *)
(* y *)
let g (ghost z: int) (x: int) : int
requires { x > 0 }
ensures { result > 0 }
= let y = x in
y
(* type t 'a 'b 'c 'd *)
type t 'a 'b 'c 'd
(* type list 'a = Nil | Cons 'a (list 'a) *)
type list 'a = Nil | Cons 'a (list 'a)
(* type btree 'a = E | N (btree 'a) 'a (btree 'a) *)
type btree 'a = E | N (btree 'a) 'a (btree 'a)
(* type ntree 'a = Empty | Node 'a (list 'a) *)
type ntree 'a = Empty | Node 'a (list 'a)
(* type list_int = list int *)
type list_int = list int
(* type cursor 'a = { *)
(* collection : list 'a; *)
(* index : int; *)
(* mutable index2 : int; *)
(* ghost mutable v : seq 'a; *)
(* } *)
type cursor 'a = {
collection : list 'a;
index : int;
mutable index2 : int;
ghost mutable v : seq 'a;
}
(* type r 'a = { *)
(* aa: 'a; *)
(* ghost i: int; *)
(* } *)
type r 'a = {
aa: 'a;
ghost i: int;
}
(* (\* let create_cursor (l: list int) (i i2: int) : cursor int = *\) *)
(* (\* { collection = l; index = i; index2 = i2; v = empty } *\) *)
(* let create_cursor (l: list int) (i i2: int) : cursor int = *)
(* { collection = l; index = i; index2 = i2; v = empty } *)
(* let create_r (x: int) (y: int) : r int = *)
(* { aa = x; i = y } *)
let create_r (x: int) (y: int) : r int =
{ aa = x; i = y }
(* use import ref.Ref *)
use import ref.Ref
(* let update (c: cursor int) : int *)
(* = c.index *)
let update (c: cursor int) : int
= c.index
(* exception Empty (list int, int) *)
(* exception Out_of_bounds int *)
exception Empty (list int, int)
exception Out_of_bounds int
(* (\* exception are unary constructors *\) *)
(* (\* *)
(* let raise1 () = *)
(* raises { Empty -> true } *)
(* raise (Empty (Nil, 0)) *)
(* let raise2 () = *)
(* raises { Empty -> true } *)
(* let p = (Nil, 0) in *)
(* raise (Empty p) *)
(* *\) *)
(* let rec length (l: list 'a) : int *)
(* variant { l } *)
(* = match l with *)
(* | Nil -> 0 *)
(* | Cons _ r -> 1 + length r *)
(* end *)
(* let t (x:int) : int *)
(* requires { false } *)
(* = absurd *)
(* let a () : unit *)
(* = assert { true } *)
(* let singleton (x: int) (l: list int) : list int = *)
(* let x = Nil in x *)
(* (\* FIXME constructors in Why3 can be partially applied *)
(* => an eta-expansion is needed *)
(* be careful with side-effects *)
(* "let c = Cons e in" should be translated to *)
(* "let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml *)
(* Mário: I think A-normal form takes care of the side-effects problem *)
(* *\) *)
(* let constructor1 () = *)
(* let x = Cons in *)
(* x 42 *)
(* let foofoo (x: int) : int = *)
(* let ghost y = x + 1 in *)
(* x *)
(* let test (x: int) : int = *)
(* let y = *)
(* let z = x in *)
(* (ghost z) + 1 *)
(* in 42 *)
(* type list_ghost = Nil2 | Cons2 int list_ghost (ghost int) *)
(* let add_list_ghost (x: int) (l: list_ghost) : list_ghost = *)
(* match l with *)
(* | Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2) *)
(* | Cons2 _ _ n -> Cons2 x l (n+1) *)
(* end *)
(* let ggg () : int = 42 *)
(* let call (x:int) : int = *)
(* ggg () + 42 *)
(* let test_filter_ghost_args (x: int) (ghost y: int) : int = *)
(* x + 42 *)
(* let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int = *)
(* x + z *)
(* let test_filter_ghost_args3 (ghost y: int) : int = *)
(* 42 *)
(* let test_call (x: int) : int = *)
(* test_filter_ghost_args x 0 *)
(* let many_args (a b c d e f g h i j k l m: int) : int = 42 *)
(* let foo (x: int) : int = *)
(* let _ = 42 in (\* FIXME? print _ in OCaml *\) *)
(* x *)
(* let test_fun (x: int) : int -> int = *)
(* fun (y: int) -> x + y *)
(* let test_partial (x: int) : int = *)
(* let partial = test_filter_ghost_args x in *)
(* partial 42 *)
(* let test_local (x: int) : int = *)
(* let fact (x: int) (y: int): int = x + y in *)
(* fact x 42 *)
(* let test_lets (x: int) : int = *)
(* let y = x in *)
(* let z = y + 1 in *)
(* let yxz = y * x * z in *)
(* let xzy = x + z + y in *)
(* let res = yxz - xzy in *)
(* res *)
(* let test_partial2 (x: int) : int = *)
(* let sum : int -> int -> int = fun x y -> x + y in *)
(* let incr_a (a: int) = sum a in *)
(* incr_a x x *)
(* let constr_partial (x: int) : list int = *)
(* let x = Cons 42 in *)
(* x Nil *)
(* let filter_record (c: cursor 'a) : int = *)
(* match c with *)
(* | { collection = l; index = i; index2 = i2; v = v} -> i *)
(* end *)
(* exception are unary constructors *)
(*
let raise1 () =
raises { Empty -> true }
raise (Empty (Nil, 0))
let raise2 () =
raises { Empty -> true }
let p = (Nil, 0) in
raise (Empty p)
*)
let rec length (l: list 'a) : int
variant { l }
= match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
let t (x:int) : int
requires { false }
= absurd
let a () : unit
= assert { true }
let singleton (x: int) (l: list int) : list int =
let x = Nil in x
(* FIXME constructors in Why3 can be partially applied
=> an eta-expansion is needed
be careful with side-effects
"let c = Cons e in" should be translated to
"let c = let o = e in fun x -> Cons (o, x) in ..." in OCaml
Mário: I think A-normal form takes care of the side-effects problem
*)
let constructor1 () =
let x = Cons in
x 42
let foofoo (x: int) : int =
let ghost y = x + 1 in
x
let test (x: int) : int =
let y =
let z = x in
(ghost z) + 1
in 42
type list_ghost = Nil2 | Cons2 int list_ghost (ghost int)
let add_list_ghost (x: int) (l: list_ghost) : list_ghost =
match l with
| Cons2 _ Nil2 _ | Nil2 -> Cons2 x Nil2 (1+2)
| Cons2 _ _ n -> Cons2 x l (n+1)
end
let ggg () : int = 42
let call (x:int) : int =
ggg () + 42
let test_filter_ghost_args (x: int) (ghost y: int) : int =
x + 42
let test_filter_ghost_args2 (x: int) (ghost y: int) (z: int) : int =
x + z
let test_filter_ghost_args3 (ghost y: int) : int =
42
let test_call (x: int) : int =
test_filter_ghost_args x 0
let many_args (a b c d e f g h i j k l m: int) : int = 42
let foo (x: int) : int =
let _ = 42 in (* FIXME? print _ in OCaml *)
x
let test_fun (x: int) : int -> int =
fun (y: int) -> x + y
let test_partial (x: int) : int =
let partial = test_filter_ghost_args x in
partial 42
let test_local (x: int) : int =
let fact (x: int) (y: int): int = x + y in
fact x 42
let test_lets (x: int) : int =
let y = x in
let z = y + 1 in
let yxz = y * x * z in
let xzy = x + z + y in
let res = yxz - xzy in
res
let test_partial2 (x: int) : int =
let sum : int -> int -> int = fun x y -> x + y in
let incr_a (a: int) = sum a in
incr_a x x
let constr_partial (x: int) : list int =
let x = Cons 42 in
x Nil
let filter_record (c: cursor 'a) : int =
match c with
| { collection = l; index = i; index2 = i2; v = v} -> i
end
end
......
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