programs: new tests in bench/programs/good/

parent ec3b9459
......@@ -242,7 +242,7 @@ clean::
# test target
%: %.mlw bin/whyml.byte
bin/whyml.byte $*.mlw
bin/whyml.byte -P alt-ergo $*.mlw
###############
# proof manager
......
(* Tests for proof obligations. *)
parameter x : int ref
{
logic q(int)
}
(* basic stuff: assignment, sequence and local variables *)
let p1 () = { q(!x+1) } begin x := !x + 1 end { q(!x) }
let p2 () = { q(7) } begin x := 3 + 4 end { q(!x) }
let p3 () = {} begin x := !x + 1; x := !x + 2 end { !x = old(!x) + 3 }
let p4 () = {} begin x := 7; x := 2 * !x end { !x = 14 }
let p5 () = {} 3 + 4 { result = 7 }
let p6 () = {} let a = 3 in a + 4 { result = 7 }
let p7 () = {} 3 + (let a = 4 in a + a) { result = 11 }
(* side effects in function arguments *)
let p8 () =
{ q(!x+1) } 3 + begin x := !x + 1; !x end { q(!x) and result = old(!x) + 4 }
(* evaluation order (argument first) *)
let p9 () =
{} begin x := 1; 1 end + begin x := 2; 1 end { result = 2 and !x = 2 }
let p9a () = {} begin x := 1; 1 end + 1 { result = 2 and !x = 1 }
(* function with a post-condition *)
parameter fsucc : x:int -> { } int { result = x + 1 }
let p10 () = {} fsucc 0 { result = 1 }
let p11 () = {} (fsucc 0) + (fsucc 3) { result = 5 }
let p11a () = {} let a = (fsucc 1) in a + a { result = 4 }
(* function with a post-condition and side-effects *)
parameter incrx : unit -> { } unit writes x { !x = old(!x) + 1 }
let p12 () = { !x = 0 } incrx () { !x = 1 }
let p13 () = {} begin incrx (); incrx () end { !x = old(!x) + 2 }
let p13a () = {} incrx (incrx ()) { !x = old(!x) + 2 }
(* function with side-effects, result and post-condition *)
parameter incrx2 : unit -> { } int writes x { !x = old(!x) + 1 and result = !x }
let p14 () = { !x = 0 } incrx2 () { result = 1 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/po"
End:
*)
......@@ -101,12 +101,30 @@ and expr_desc env loc ty = function
let e2 = expr env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Elet (v, e1, e2), e2.expr_type_v, ef
| Pgm_ttree.Eletrec _ ->
assert false (*TODO*)
| Pgm_ttree.Esequence (e1, e2) ->
let e1 = expr env e1 in
let e2 = expr env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Esequence (e1, e2), e2.expr_type_v, ef
| Pgm_ttree.Eif _ ->
assert false (*TODO*)
| Pgm_ttree.Ewhile _ ->
assert false (*TODO*)
| Pgm_ttree.Elazy _ ->
assert false (*TODO*)
| Pgm_ttree.Ematch _ ->
assert false (*TODO*)
| Pgm_ttree.Eskip ->
Eskip, Tpure ty, E.empty
| Pgm_ttree.Eabsurd ->
assert false (*TODO*)
| Pgm_ttree.Eraise _ ->
assert false (*TODO*)
| Pgm_ttree.Etry _ ->
assert false (*TODO*)
| Pgm_ttree.Eassert (k, f) ->
let ef = fmla_effect env E.empty f in
......@@ -114,8 +132,7 @@ and expr_desc env loc ty = function
| Pgm_ttree.Elabel (lab, e1) ->
let e1 = expr env e1 in
Elabel (lab, e1), e1.expr_type_v, e1.expr_effect
| _ ->
| Pgm_ttree.Eany _ ->
assert false (*TODO*)
and triple env (p, e, q) =
......@@ -303,8 +320,7 @@ and wp_desc env e q = match e.expr_desc with
| Elocal _ ->
assert false (*TODO*)
| Eglobal _ ->
let (_, q), _ = q in
q
let (_, q), _ = q in q
| Efun (bl, t) ->
let (_, q), _ = q in
let f = wp_triple env t in
......@@ -322,6 +338,22 @@ and wp_desc env e q = match e.expr_desc with
let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
wp_expr env e1 q1
| Eif _ ->
assert false (*TODO*)
| Ewhile _ ->
assert false (*TODO*)
| Elazy _ ->
assert false (*TODO*)
| Ematch _ ->
assert false (*TODO*)
| Eskip ->
let (_, q), _ = q in q
| Eabsurd ->
assert false (*TODO*)
| Eraise _ ->
assert false (*TODO*)
| Etry _ ->
assert false (*TODO*)
| Eassert (Pgm_ptree.Aassert, f) ->
let (_, q), _ = q in
......@@ -340,7 +372,7 @@ and wp_desc env e q = match e.expr_desc with
wp_and c.c_pre w
| _ ->
f_true (* TODO *)
assert false (*TODO*)
and wp_triple env (p, e, q) =
let f = wp_expr env e q in
......
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