new program example decrease1

parent 41f05be4
(*
We look for the first occurrence of zero in an array of integers.
The values have the following property: they never decrease by more than one.
The code makes use of that property to speed up the search.
*)
module Decrease1
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
logic decrease1 (a: array int) =
forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
lemma decrease1_induction:
forall a: array int. decrease1 a ->
forall i j: int. 0 <= i <= j < length a -> a[j] >= a[i] + i - j
exception Found int
let search (a: array int) =
{ decrease1 a }
let i = ref 0 in
while !i < length a do
invariant { 0 <= i and forall j: int. 0 <= j < i -> a[j] <> 0 }
variant { length a - i }
if get a !i = 0 then raise (Found !i);
if get a !i > 0 then i := !i + get a !i else i := !i + 1
done
{ forall j: int. 0 <= j < length a -> a[j] <> 0 }
| Found -> { 0 <= result < length a and a[result] = 0 and
forall j: int. 0 <= j < result -> a[j] <> 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/decrease1.gui"
End:
*)
......@@ -41,8 +41,8 @@ let rec print_expr fmt e = match e.expr_desc with
fprintf fmt "<todo: Elabel>"
| Eassert (_, f) ->
fprintf fmt "@[assert {%a}@]" print_fmla f
| Efor (_, _, _, _, _, _) ->
fprintf fmt "<todo: Efor>"
| Efor (_, _, _, _, _, e) ->
fprintf fmt "@[<hov 2>for ... do@ %a@ done@]" print_expr e
| Etry (_, _) ->
fprintf fmt "<todo: Etry>"
| Eraise (_, _) ->
......
......@@ -172,8 +172,8 @@ let has_singleton_type pv = is_singleton_ty pv.pv_effect.vs_ty
*)
let quantify ?(all=false) env rm ef f =
(* eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@]@]@." *)
(* all E.print ef Pretty.print_fmla f; *)
eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@]@]@."
all E.print ef Pretty.print_fmla f;
let sreg = ef.E.writes in
let sreg =
if all then
......@@ -204,8 +204,10 @@ let quantify ?(all=false) env rm ef f =
let v = create_vsymbol (id_clone pv.pv_name) (purify r.R.r_ty) in
let mreg = Mreg.add r v mreg in
mreg, Mvs.add pv.pv_pure v s, vv'
end else
end else begin
eprintf "pv = %a@." print_pvsymbol pv;
assert false (*TODO*)
end
in
Spv.fold add vars (mreg, Mvs.empty, Mpv.empty)
in
......@@ -543,7 +545,7 @@ and wp_triple env rm bl (p, e, q) =
in
let f = wp_expr env rm e q in
let f = wp_implies p f in
let f = quantify ~all:true env rm e.expr_effect f in
let f = quantify (* ~all:true *) env rm e.expr_effect f in
wp_binders bl f
and wp_recfun env rm (_, bl, _var, t) =
......
module Alg
module M
type t = A
use import int.Int
use import module stdlib.Ref
let foo () = match A with A -> () end
let test1 () =
let x = ref 0 in
while True do
invariant { 0 <= x }
x := !x + 1
done
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