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.31

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.5CVC5 1.0.0
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------0.08
postcondition------0.11
VC for create---0.02---
VC for query_aux---0.25---
VC for query------0.06
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------0.10
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---