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.12.2
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.07

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.12.2
VC for create---0.01
VC for query0.06---
VC for update---0.24

Theory "sumrange.CumulativeTree": fully verified

ObligationsAlt-Ergo 2.3.3Alt-Ergo 2.4.3CVC4 1.5CVC5 1.0.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---------0.19
postcondition---------0.26
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.0------------
split_vc
is_tree_for_frame.0.0---1.22------
is_tree_for_frame.0.1---2.11------
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.72---
VC for update---------0.24
depth_min------------
induction_ty_lex
depth_min.0------0.03---
VC for depth_is_log0.51---------
VC for update_aux_complexity------------
split_goal_right
assertion------0.04---
postcondition------0.02---
postcondition------0.30---
variant decrease------0.04---
precondition------0.04---
precondition------0.05---
assertion------0.04---
assertion------0.04---
postcondition------0.04---
postcondition------0.78---
variant decrease------0.02---
precondition------0.03---
precondition------0.04---
assertion------0.04---
assertion------0.03---
postcondition------0.04---
postcondition------0.79---
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---