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

## 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.12.2 VC for create --- 0.01 VC for query 0.06 --- VC for update --- 0.24

## Theory "sumrange.CumulativeTree": fully verified

 Obligations Alt-Ergo 2.3.3 Alt-Ergo 2.4.3 CVC4 1.5 CVC5 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_log 0.51 --- --- --- 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 ---