theory int.Sum with excluded right bound

this is consistent with other, similar theories
parent 82471364
......@@ -60,14 +60,14 @@ module TestCursor
let sum (t: t) (c: cursor) : int
requires { coherent t c }
requires { c.i = 0 }
ensures { result = sum 0 (length c.seq - 1) (get c.seq) }
ensures { result = sum 0 (length c.seq) (get c.seq) }
let s = ref 0 in
while has_next t c do
invariant { coherent t c }
invariant { 0 <= c.i <= length c.seq }
invariant { !s = sum 0 (c.i - 1) (get c.seq) }
invariant { !s = sum 0 c.i (get c.seq) }
variant { length c.seq - c.i }
let x = next t c in
s += x
......@@ -7,12 +7,12 @@
<prover id="2" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" memlimit="1000"/>
<file name="../cursor.mlw" expanded="true">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../cursor.mlw">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="TestCursor" sum="176c55ab5c9e377bb55c280a95c35887" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<transf name="split_goal_wp" expanded="true">
<theory name="TestCursor" sum="b7657686cab5c94f3d90eee7eca8293b">
<goal name="WP_parameter sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="WP_parameter sum.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="2"/></proof>
......@@ -20,7 +20,7 @@
<goal name="WP_parameter sum.2" expl="2. loop invariant init">
<proof prover="3"><result status="valid" time="0.02" steps="3"/></proof>
<goal name="WP_parameter sum.3" expl="3. loop invariant init" expanded="true">
<goal name="WP_parameter sum.3" expl="3. loop invariant init">
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
<goal name="WP_parameter sum.4" expl="4. precondition">
......@@ -43,14 +43,14 @@
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
<goal name="WP_parameter sum.9" expl="9. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="17"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
<goal name="WP_parameter sum.10" expl="10. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
<goal name="WP_parameter sum.11" expl="11. postcondition" expanded="true">
<goal name="WP_parameter sum.11" expl="11. postcondition">
<proof prover="3"><result status="valid" time="0.02" steps="8"/></proof>
......@@ -100,22 +100,22 @@
<theory name="IntArrayCursor" sum="c77cddb83b83b50f0453ae017ebaaabf" expanded="true">
<theory name="IntArrayCursor" sum="c77cddb83b83b50f0453ae017ebaaabf">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter has_next" expl="VC for has_next">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter reverse_cons" expl="VC for reverse_cons" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter reverse_cons" expl="VC for reverse_cons">
<transf name="split_goal_wp">
<goal name="WP_parameter reverse_cons.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter reverse_cons.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter reverse_cons.3" expl="3. postcondition" expanded="true">
<goal name="WP_parameter reverse_cons.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<goal name="WP_parameter reverse_cons.4" expl="4. postcondition">
......@@ -141,7 +141,7 @@
<theory name="TestArrayCursor" sum="1e7488f16d72fe3b07df3520264bcf37" expanded="true">
<theory name="TestArrayCursor" sum="a6e72a6cc7801f1991c45b6d2715367e">
<goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list">
<proof prover="1"><result status="valid" time="0.04"/></proof>
......@@ -176,29 +176,9 @@
<goal name="WP_parameter harness1" expl="VC for harness1" expanded="true">
<goal name="WP_parameter harness1" expl="VC for harness1">
<proof prover="4"><result status="valid" time="0.23"/></proof>
<goal name="WP_parameter harness2" expl="VC for harness2" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter harness2.1" expl="1. array creation size">
<proof prover="3"><result status="valid" time="0.03" steps="1"/></proof>
<goal name="WP_parameter harness2.2" expl="2. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
<goal name="WP_parameter harness2.3" expl="3. precondition" expanded="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<goal name="WP_parameter harness2.4" expl="4. precondition" expanded="true">
<proof prover="3"><result status="timeout" time="9.98"/></proof>
<proof prover="4"><result status="timeout" time="11.01"/></proof>
<goal name="WP_parameter harness2.5" expl="5. assertion" expanded="true">
<proof prover="4"><result status="valid" time="0.28"/></proof>
......@@ -347,38 +347,38 @@ theory Sum
use HighOrd
function sum (a b: int) (f: int -> int) : int
(** sum of [f n] for [a <= n <= b] *)
(** sum of [f n] for [a <= n < b] *)
axiom sum_def1:
forall f: int -> int, a b: int.
b < a -> sum a b f = 0
b <= a -> sum a b f = 0
axiom sum_def2:
forall f: int -> int, a b: int.
a <= b -> sum a b f = sum a (b - 1) f + f b
a < b -> sum a b f = sum a (b - 1) f + f (b - 1)
lemma sum_left:
forall f: int -> int, a b: int.
a <= b -> sum a b f = f a + sum (a + 1) b f
a < b -> sum a b f = f a + sum (a + 1) b f
lemma sum_ext:
forall f g: int -> int, a b: int.
(forall i. a <= i <= b -> f i = g i) ->
(forall i. a <= i < b -> f i = g i) ->
sum a b f = sum a b g
lemma sum_le:
forall f g: int -> int, a b: int.
(forall i. a <= i <= b -> f i <= g i) ->
(forall i. a <= i < b -> f i <= g i) ->
sum a b f <= sum a b g
lemma sum_nonneg:
forall f: int -> int, a b: int.
(forall i. a <= i <= b -> 0 <= f i) ->
(forall i. a <= i < b -> 0 <= f i) ->
0 <= sum a b f
lemma sum_decomp:
forall f: int -> int, a b c: int. a <= b <= c ->
sum a c f = sum a b f + sum (b+1) c f
sum a c f = sum a b f + sum b c f
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