Sum queries
Get sum of values in array ranges, efficient algorithms
Auteurs: Claude Marché
Catégories: Array Data Structure / Ghost code
Outils: 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
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 | --- |