## 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)

# Why3 Proof Results for Project "sumrange"

## Theory "sumrange.ArraySum": fully verified

 Obligations CVC4 1.5 Z3 4.5.0 VC for sum 0.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

 Obligations CVC4 1.5 VC for query --- split_goal_right loop invariant init 0.02 index in array bounds 0.01 loop invariant preservation 0.02 postcondition 0.00 out of loop bounds 0.02

## Theory "sumrange.ExtraLemmas": fully verified

 Obligations CVC4 1.5 sum_concat --- introduce_premises sum_concat.0 --- induction k base case 0.01 recursive case --- instantiate Hrec k recursive case 0.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.0 0.00 sum_update --- introduce_premises sum_update.0 --- induction h from i+1 base case --- compute_in_goal base case 0.07 recursive case --- compute_in_goal recursive case 0.04

## Theory "sumrange.CumulativeArray": fully verified

 Obligations CVC4 1.5 Z3 4.5.0 VC for create --- 0.02 VC for query 0.06 --- VC for update --- 0.05

## Theory "sumrange.CumulativeTree": fully verified

 Obligations Alt-Ergo 2.0.0 CVC4 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.0 1.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_log 0.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