Commit 6d5bd39a authored by Clément Fumex's avatar Clément Fumex
Browse files

Merge branch 'master' into bv_rea_clem

parents 2da66405 23ef5a93
......@@ -214,7 +214,6 @@ pvsbin/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/next_digit_sum/
/examples/in_progress/vacid_0_red_black_trees_harness/
/examples/why3bench.html
/examples/why3regtests.err
......
......@@ -35,14 +35,18 @@ module M
(* to allow provers to prove that an assignment does not change the
interpretation on the left (or on the right); requires induction *)
lemma Interp_eq:
forall x1 x2 : M.map int int, i j : int.
(forall k : int. i <= k < j -> M.get x1 k = M.get x2 k) ->
interp x1 i j = interp x2 i j
let rec lemma interp_eq
(x1 x2 : M.map int int) (i j : int)
requires { forall k : int. i <= k < j -> M.get x1 k = M.get x2 k }
ensures { interp x1 i j = interp x2 i j }
variant { j - i }
= if i < j then interp_eq x1 x2 (i+1) j
(* the sum of the elements of x[i..j[ *)
type map_int = M.map int int
clone export sum.Sum with type container = map_int, function f = M.get
use int.Sum
function sum (m: M.map int int) (i j: int) : int =
Sum.sum i (j - 1) (\ k: int. M.get m k)
lemma Sum_is_sum_digits_interp:
forall x : M.map int int, i j : int.
......
This diff is collapsed.
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