Wiki Agenda Contact Version française

Sum queries

Get sum of values in array ranges, efficient algorithms


Authors: Claude Marché

Topics: Array Data Structure / Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


download ZIP archive

Why3 Proof Results for Project "sumrange"

Theory "sumrange.ArraySum": fully verified

ObligationsCVC4 1.5Z3 4.5.0
VC for sum0.01---
sum_right------
introduce_premises
sum_right.0------
assert (forall x. 0 < x < j -> sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])
asserted formula------
introduce_premises
asserted formula------
induction x
base case (asserted formula)0.00---
recursive case (asserted formula)------
instantiate Hrec (x - 1)
recursive case (asserted formula)0.02---
sum_right.0.1------
instantiate h (j-i)
sum_right.0.1.0---0.10

Theory "sumrange.Simple": fully verified

ObligationsCVC4 1.5
VC for query---
split_goal_right
loop invariant init0.02
index in array bounds0.01
loop invariant preservation0.02
postcondition0.00
out of loop bounds0.02

Theory "sumrange.ExtraLemmas": fully verified

ObligationsCVC4 1.5
sum_concat---
introduce_premises
sum_concat.0---
induction k
base case0.01
recursive case---
instantiate Hrec k
recursive case0.02
sum_frame---
introduce_premises
sum_frame.0---
assert (forall x. 0 <= x <= j-i -> sum a1 (j-x) j = sum a2 (j-x) j)
asserted formula---
introduce_premises
asserted formula---
induction x
base case (asserted formula)0.01
recursive case (asserted formula)---
instantiate Hrec (x - 1)
recursive case (asserted formula)0.02
sum_frame.0.1---
instantiate h (j-i)
sum_frame.0.1.00.00
sum_update---
introduce_premises
sum_update.0---
induction h from i+1
base case---
compute_in_goal
base case0.07
recursive case---
compute_in_goal
recursive case0.04

Theory "sumrange.CumulativeArray": fully verified

ObligationsCVC4 1.5Z3 4.5.0
VC for create---0.02
VC for query0.06---
VC for update---0.05

Theory "sumrange.CumulativeTree": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5
VC for tree_of_array------
split_goal_right
index in array bounds---0.02
precondition---0.01
assertion---0.03
variant decrease---0.02
precondition---0.02
variant decrease---0.02
precondition---0.02
assertion------
introduce_premises
assertion------
destruct_term l
assertion------
destruct_term r
assertion---0.08
assertion---0.04
assertion------
destruct_term r using b1,b2,b3
assertion---0.11
assertion---0.04
postcondition------
split_goal_right
postcondition---0.02
postcondition------
unfold is_tree_for
VC for tree_of_array---0.22
VC for create---0.02
VC for query_aux---0.25
VC for query------
introduce_premises
VC for query------
destruct_term t
VC for query---0.03
VC for query---0.04
is_tree_for_frame------
induction_ty_lex
is_tree_for_frame.01.17---
VC for update_aux------
split_goal_right
assertion---0.05
variant decrease---0.03
precondition---0.02
precondition---0.04
assertion---0.03
assertion---0.04
variant decrease---0.03
precondition---0.04
precondition---0.03
assertion---0.03
assertion---0.03
postcondition---0.55
VC for update------
introduce_premises
VC for update------
destruct_term t
VC for update---0.04
VC for update---0.03
depth_min------
induction_ty_lex
depth_min.0---0.03
VC for depth_is_log0.77---
VC for update_aux_complexity------
split_goal_right
assertion---0.04
postcondition---0.02
postcondition---0.09
variant decrease---0.04
precondition---0.04
precondition---0.05
assertion---0.04
assertion---0.04
postcondition---0.04
postcondition---0.12
variant decrease---0.02
precondition---0.03
precondition---0.04
assertion---0.04
assertion---0.03
postcondition---0.04
postcondition---0.13
VC for query_aux_complexity------
split_goal_right
postcondition---0.04
postcondition---0.05
postcondition---0.03
postcondition---0.06
variant decrease---0.04
precondition---0.03
precondition---0.04
postcondition---0.04
postcondition---0.02
variant decrease---0.04
precondition---0.04
precondition---0.04
postcondition---0.05
postcondition---0.02
variant decrease---0.05
precondition---0.04
precondition---0.04
variant decrease---0.04
precondition---0.04
precondition---0.04
postcondition---0.03
postcondition---0.06