Commit e5c887c7 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into new_system

# Conflicts:
#	Makefile.in
#	Version
#	examples/avl/priority_queue/why3session.xml
#	examples/avl/priority_queue/why3shapes.gz
#	examples/avl/tables/why3session.xml
#	examples/avl/tables/why3shapes.gz
#	examples/binomial_heap/why3session.xml
#	examples/binomial_heap/why3shapes.gz
#	examples/bitcount/why3session.xml
#	examples/bitcount/why3shapes.gz
#	examples/counting_sort/why3session.xml
#	examples/counting_sort/why3shapes.gz
#	examples/dijkstra/why3shapes.gz
#	examples/double_wp/compiler/why3session.xml
#	examples/double_wp/compiler/why3shapes.gz
#	examples/double_wp/specs/why3session.xml
#	examples/double_wp/specs/why3shapes.gz
#	examples/dyck/why3session.xml
#	examples/dyck/why3shapes.gz
#	examples/euler001/why3session.xml
#	examples/euler001/why3shapes.gz
#	examples/euler011/why3session.xml
#	examples/euler011/why3shapes.gz
#	examples/finger_trees/why3session.xml
#	examples/finger_trees/why3shapes.gz
#	examples/hashtbl_impl/why3shapes.gz
#	examples/inverse_in_place/why3session.xml
#	examples/inverse_in_place/why3shapes.gz
#	examples/knuth_prime_numbers/why3session.xml
#	examples/knuth_prime_numbers/why3shapes.gz
#	examples/koda_ruskey/why3session.xml
#	examples/koda_ruskey/why3shapes.gz
#	examples/linear_probing/why3session.xml
#	examples/linear_probing/why3shapes.gz
#	examples/linked_list_rev/why3session.xml
#	examples/linked_list_rev/why3shapes.gz
#	examples/logic/triangle_inequality/why3session.xml
#	examples/logic/triangle_inequality/why3shapes.gz
#	examples/max_matrix/why3session.xml
#	examples/max_matrix/why3shapes.gz
#	examples/maximum_subarray/why3session.xml
#	examples/maximum_subarray/why3shapes.gz
#	examples/mergesort_list/why3session.xml
#	examples/mergesort_list/why3shapes.gz
#	examples/power/why3session.xml
#	examples/power/why3shapes.gz
#	examples/quicksort/why3session.xml
#	examples/quicksort/why3shapes.gz
#	examples/register_allocation/why3session.xml
#	examples/register_allocation/why3shapes.gz
#	examples/ropes/why3session.xml
#	examples/ropes/why3shapes.gz
#	examples/schorr_waite/why3session.xml
#	examples/schorr_waite/why3shapes.gz
#	examples/schorr_waite_via_recursion/why3session.xml
#	examples/schorr_waite_via_recursion/why3shapes.gz
#	examples/stdlib/array/why3session.xml
#	examples/tests-provers/bv/why3session.xml
#	examples/tests-provers/div/why3session.xml
#	examples/to_port/dijkstra.mlw
#	examples/to_port/dijkstra/why3session.xml
#	examples/to_port/hashtbl_impl/why3session.xml
#	examples/verifythis_2015_relaxed_prefix/why3session.xml
#	examples/verifythis_2015_relaxed_prefix/why3shapes.gz
#	examples/verifythis_2016_tree_traversal/why3session.xml
#	examples/verifythis_2016_tree_traversal/why3shapes.gz
#	examples/vstte12_combinators/why3session.xml
#	examples/vstte12_combinators/why3shapes.gz
#	examples/vstte12_ring_buffer/why3session.xml
#	examples/vstte12_ring_buffer/why3shapes.gz
#	examples/vstte12_two_way_sort/why3session.xml
#	examples/vstte12_two_way_sort/why3shapes.gz
#	src/core/ident.ml
#	src/core/pretty.ml
#	src/core/pretty.mli
#	src/core/trans.ml
#	src/ide/gmain.ml
#	src/parser/lexer.mli
#	src/parser/lexer.mll
#	src/parser/parser.mly
#	src/parser/typing.ml
#	src/parser/typing.mli
#	src/session/session.ml
#	src/session/session_scheduler.ml
#	src/session/session_scheduler.mli
#	src/tools/why3replay.ml
#	src/transform/introduction.ml
#	src/util/pp.mli
#	src/util/strings.ml
#	src/why3session/why3session_html.ml
#	src/whyml/mlw_interp.ml
parents d754ddee d6bd47f9
......@@ -84,9 +84,15 @@ why3.conf
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
/bin/why3shell.opt
/bin/why3shell.byte
/bin/why3shell
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
# /doc/
/doc/version.tex
......@@ -199,6 +205,7 @@ pvsbin/
/src/util/config.ml
/src/util/lexlib.ml
/src/util/rc.ml
/src/util/json_lexer.ml
/src/util/json_parser.mli
/src/util/json_parser.ml
......@@ -210,6 +217,10 @@ pvsbin/
# /src/tools
/src/tools/why3wc.ml
# /src/ide
/src/ide/why3_js.byte
/src/ide/why3_js.js
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
......
......@@ -20,6 +20,7 @@ Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
......
* marks an incompatible change
Version 0.88.0, October 6, 2017
===============================
Language
o two new forms of type declarations: integer range types and
floating-point types. To denote constants in such types, integer
constants and real constants can be cast to such types. This
support is exploited in drivers for provers that support bitvector
theories (CVC4, Z3) and floating-point theory (Z3).
More details in the manual, section 7.2.4 "Theories"
More details in the manual, section 7.2.4 "Theories".
* a quote character (') inside an identifier must either be at the
end, or be followed by either a digit, the underscore character
(_) or another quote. Identifiers with a quote followed by a
......@@ -15,19 +18,18 @@ Language
Standard library
o new theory ieee_float formalizing floating-point arithmetic,
conformant to IEEE-754, mapped to SMT-LIB FP theory.
compliant to IEEE-754, mapped to SMT-LIB FP theory.
User features
o proof strategies: why3 config now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide. More
details in the manual, section 10.6 "Proof Strategies"
o counterexamples: better support for array
values, support for floating-point values, support for Z3 in
addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples"
Prover support
level 0", "Auto level 1" and "Auto level 2" in why3 ide.
More details in the manual, section 10.6 "Proof Strategies".
o counterexamples: better support for array values, support for
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Provers
o support for Isabelle 2017
* discarded support for Isabelle 2016 (2016-1 still supported)
o support for Coq 8.6.1 (released Jul 25, 2017)
......@@ -40,11 +42,11 @@ Prover support
Version 0.87.3, January 12, 2017
================================
bug fixes
Bug fixes
o fixed OCaml extraction with respect to ghost parameters
o assorted bug fixes
provers
Provers
o support for Alt-Ergo 1.30 (released Nov 21, 2016)
o support for Coq 8.6 (released Dec 8, 2016)
o support for Gappa 1.3 (released Jul 20, 2016)
......@@ -55,14 +57,14 @@ provers
Version 0.87.2, September 1, 2016
=================================
bug fixes
Bug fixes
o improved well-formedness of extracted OCaml code
o assorted bug fixes
Version 0.87.1, May 27, 2016
============================
bug fixes
Bug fixes
o assorted bug fixes
Version 0.87.0, March 15, 2016
......
......@@ -149,7 +149,10 @@ GENERATED =
##############
LIBGENERATED = src/util/config.ml \
src/util/rc.ml src/util/lexlib.ml src/parser/lexer.ml \
src/util/rc.ml src/util/lexlib.ml \
src/util/json_parser.mli src/util/json_parser.ml \
src/util/json_lexer.ml \
src/parser/lexer.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml \
......@@ -161,11 +164,13 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
pp extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer json debug loc lexlib print_tree \
hashcons stdlib exn_printer \
json_base json_parser json_lexer \
debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl coercion theory \
task pretty dterm env trans printer model_parser
task pretty_sig pretty dterm env trans printer model_parser
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
......@@ -190,14 +195,18 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_epsilon intro_projections_counterexmp \
intro_vc_vars_counterexmp prepare_for_counterexmp \
instantiate_predicate smoke_detector \
induction_pr prop_curry eliminate_literal
induction_pr prop_curry eliminate_literal \
args_wrapper generic_arg_trans_utils case apply \
ind_itp destruct cut
LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\
pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_SESSION = compress xml termcode session session_tools strategy \
strategy_parser session_scheduler
LIB_SESSION = compress xml termcode session_itp \
strategy strategy_parser controller_itp \
server_utils itp_communication \
itp_server json_util
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
......@@ -517,8 +526,8 @@ bin/why3prove.opt: lib/why3/why3.cmxa src/tools/why3prove.cmx
bin/why3prove.byte: lib/why3/why3.cma src/tools/why3prove.cmo
bin/why3realize.opt: lib/why3/why3.cmxa src/tools/why3realize.cmx
bin/why3realize.byte: lib/why3/why3.cma src/tools/why3realize.cmo
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/why3replay.cmx
bin/why3replay.byte: lib/why3/why3.cma src/tools/why3replay.cmo
bin/why3replay.opt: lib/why3/why3.cmxa src/tools/unix_scheduler.cmx src/tools/why3replay.cmx
bin/why3replay.byte: lib/why3/why3.cma src/tools/unix_scheduler.cmo src/tools/why3replay.cmo
bin/why3wc.opt: src/tools/why3wc.cmx
bin/why3wc.byte: src/tools/why3wc.cmo
......@@ -700,7 +709,7 @@ xml-validate-local:
ifeq (@enable_ide@,yes)
IDE_FILES = gconfig gmain
IDE_FILES = gconfig ide_utils why3ide
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -751,14 +760,63 @@ install_local:: bin/why3ide
endif
###############
# WEBSERV
###############
WEBSERV_FILES = wserver why3web
WEBSERVMODULES = $(addprefix src/ide/, $(WEBSERV_FILES))
WEBSERVDEP = $(addsuffix .dep, $(WEBSERVMODULES))
WEBSERVCMO = $(addsuffix .cmo, $(WEBSERVMODULES))
WEBSERVCMX = $(addsuffix .cmx, $(WEBSERVMODULES))
$(WEBSERVDEP): DEPFLAGS += -I src/ide
$(WEBSERVCMO) $(WEBSERVCMX): INCLUDES += -I src/ide
# build targets
byte: bin/why3webserver.byte
opt: bin/why3webserver.opt
bin/why3webserver.opt: lib/why3/why3.cmxa $(WEBSERVCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3webserver.byte: lib/why3/why3.cma $(WEBSERVCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) -custom $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(WEBSERVDEP)
endif
depend: $(WEBSERVDEP)
CLEANDIRS += src/ide
clean_old_install::
rm -f $(BINDIR)/why3webserver$(EXE)
install_no_local::
$(INSTALL) bin/why3webserver.@OCAMLBEST@ $(TOOLDIR)/why3webserver$(EXE)
install_local:: bin/why3webserver
###############
# Session
###############
SESSION_FILES = why3session_lib why3session_copy why3session_info \
why3session_latex why3session_html why3session_rm \
why3session_output why3session_run why3session_csv \
SESSION_FILES = why3session_lib why3session_info \
why3session_html why3session_latex \
why3session_main
# TODO: why3session_copy why3session_rm why3session_csv why3session_run
# why3session_output
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
......@@ -800,6 +858,50 @@ install_no_local::
install_local:: bin/why3session
###############
# Why3 Shell
###############
SHELL_FILES = unix_scheduler why3shell
SHELLMODULES = $(addprefix src/tools/, $(SHELL_FILES))
SHELLDEP = $(addsuffix .dep, $(SHELLMODULES))
SHELLCMO = $(addsuffix .cmo, $(SHELLMODULES))
SHELLCMX = $(addsuffix .cmx, $(SHELLMODULES))
$(SHELLDEP): DEPFLAGS += -I src/tools
$(SHELLCMO) $(SHELLCMX): INCLUDES += -I src/tools
# build targets
byte: bin/why3shell.byte
opt: bin/why3shell.opt
bin/why3shell.opt: lib/why3/why3.cmxa $(SHELLCMX)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3shell.byte: lib/why3/why3.cma $(SHELLCMO)
$(SHOW) 'Linking $@'
$(HIDE)$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
-include $(SHELLDEP)
endif
depend: $(SHELLDEP)
clean_old_install::
rm -f $(BINDIR)/why3shell$(EXE)
install_no_local::
$(INSTALL) bin/why3shell.@OCAMLBEST@ $(TOOLDIR)/why3shell$(EXE)
install_local:: bin/why3shell
##############
# Coq plugin
......@@ -1557,7 +1659,6 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
......@@ -1567,7 +1668,6 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
......@@ -1592,6 +1692,30 @@ clean::
CLEANDIRS += src/trywhy3
#########
# why3webserver and full web/js interface
#########
ifeq (@HASJSOFOCAML,yes)
JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.ppx \
-I src/ide
src/ide/why3_js.cmo: src/ide/why3_js.ml lib/why3/why3.cma
$(JSOCAMLCW) $(BFLAGS) -c $<
src/ide/why3_js.byte: lib/why3/why3.cma src/ide/why3_js.cmo
$(JSOCAMLCW) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3_js.js: src/ide/why3_js.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
endif
########
# bench
########
......@@ -1619,6 +1743,10 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# test targets
###############
test-itp.opt: src/printer/itp.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \
$(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $<
test-api-logic.byte: examples/use_api/logic.ml lib/why3/why3.cma
$(SHOW) 'Ocaml $<'
$(HIDE)ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< > /dev/null \
......@@ -1773,9 +1901,13 @@ MODULESTODOC = \
util/extmap util/extset util/exthtbl \
util/weakhtbl util/stdlib util/rc util/debug \
core/ident core/ty core/term core/decl core/coercion core/theory \
core/env core/task \
core/env core/task core/trans \
driver/whyconf driver/call_provers driver/driver \
session/session session/session_tools session/session_scheduler
transform/args_wrapper \
session/session_itp session/controller_itp \
session/itp_communication session/itp_server \
whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
whyml/mlw_wp
FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
......@@ -1918,7 +2050,7 @@ clean::
# the generic rule cannot be applied since ocaml would confuse
# lib/why3/why3extract.cmi for the interface (!!!)
# same for ocaml/lablgtk2/gMain.cmi on case-insensitive filesystems
src/tools/why3extract.cmx src/ide/gmain.cmx: %.cmx: %.ml
src/tools/why3extract.cmx: %.cmx: %.ml
$(SHOW) 'Ocamlopt $<'
$(HIDE)$(OCAMLOPT) -c $(OFLAGS) $<
......
# Why version
VERSION=0.90+git
......@@ -476,6 +476,18 @@ dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# js_of_ocaml
JSOFOCAML=$(ocamlfind query js_of_ocaml)
if test -z "$JSOFCAML"; then
HASJSOFOCAML=no
reason_jsofocaml=" (js_of_ocaml not found)"
else
HASJSOFOCAML=yes
fi
# Coq
enable_coq_support=yes
......@@ -770,6 +782,8 @@ AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)
AC_SUBST(HASJSOFOCAML)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(enable_zarith)
......@@ -860,7 +874,8 @@ echo " Library path : $OCAMLLIB"
echo " Native compilation : $enable_native_code"
echo " Profiling : $enable_profiling"
echo "Components"
echo " IDE command : $enable_ide$reason_ide"
echo " GTK IDE : $enable_ide$reason_ide"
echo " Web IDE : $HASJSOFOCAML$reason_jsofocaml"
echo " GMP arithmetic : $enable_zarith$reason_zarith"
echo " Compressed sessions : $enable_zip$reason_zip"
echo " MenhirLib support : $enable_menhirLib$reason_menhirLib"
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, January 2017
Version \whyversion{}, October 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
module Exp
use import ieee_float.Float64
use import real.Abs
use import real.ExpLog
use import real.Real
val ( +. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .+ y)}
ensures {result = x .+ y}
val ( *. ) (x y : t) : t
requires {t'isFinite x}
requires {t'isFinite y}
requires {"expl:no_overflow" t'isFinite (x .* y)}
ensures {result = x .* y}
let my_exp (x: t) : t
requires { t'isFinite x}
requires { .- (1.0:t) .<= x .<= (1.0:t)}
requires {abs (t'real x) <= 1.0}
ensures { abs (t'real result - exp (t'real x)) <= 0x1p-4} (* 1 * 2 ^ - 4 *)
=
assert {
let x = t'real x in
abs(0.9890365552 + 1.130258690*x +
0.5540440796*x*x - exp(x)) <= 0x0.FFFFp-4};
(0x1.FA62FFD643D6Ep-1:t) +. (0x1.2158A22D91DE9p0:t) *. x +.
(0x1.1BABAA64D94DBp-1:t) *. x *. x
end
......@@ -38,7 +38,7 @@ ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDEALL) -I ../../../plugins/tptp
LIBS=unix.cmxa nums.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
LIBS=unix.cmxa $(BIGINTLIB).cmxa dynlink.cmxa str.cmxa menhirLib.cmx zip.cmxa why3.cmxa why3extract.cmxa tptp_ast.cmx tptp_typing.cmx tptp_parser.cmx tptp_lexer.cmx
LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
WHY3FLAGS=-L . --debug ignore_unused_vars
MLFLAGS=
......
(** {1 Range Sum Queries}
We are interested in specifying and proving correct
data structures that support efficient computation of the sum of the
values over an arbitrary range of an array.
Concretely, given an array of integers [a], and given a range
delimited by indices [i] (inclusive) and [j] (exclusive), we wish
to compute the value: [\sum_{k=i}^{j-1} a[k]].
In the first part, we consider a simple loop
for computing the sum in linear time.
In the second part, we introduce a cumulative sum array
that allows answering arbitrary range queries in constant time.
In the third part, we explore a tree data structure that
supports modification of values from the underlying array [a],
with logarithmic time operations.
*)
(** {2 Specification of Range Sum} *)
module ArraySum
use export int.Int
use export array.Array
(** [sum a i j] denotes the sum [\sum_{i <= k < j} a[k]].
It is axiomatizated by the two following axioms expressing
the recursive definition
if [i <= j] then [sum a i j = 0]
if [i < j] then [sum a i j = a[i] + sum a (i+1) j]
*)
function sum (array int) int int : int
axiom sum_def_empty :
forall a : array int, i j : int. j <= i -> sum a i j = 0
axiom sum_def_non_empty :
forall a: array int, i j : int. i < j /\ 0 <= i < a.length ->
sum a i j = a[i] + sum a (i+1) j
(** lemma for summation from the right:
if [i < j] then [sum a i j = sum a i (j-1) + a[j-1]]
*)
lemma sum_right : forall a : array int, i j : int.
0 <= i < j <= a.length ->
sum a i j = sum a i (j-1) + a[j-1]
end
(** {2 First algorithm, a linear one} *)
module Simple
use import ArraySum
use import ref.Ref
(** [query a i j] returns the sum of elements in [a] between
index [i] inclusive and index [j] exclusive *)
let query (a:array int) (i j:int) : int
requires { 0 <= i <= j <= a.length }
ensures { result = sum a i j }
= let s = ref 0 in
for k=i to j-1 do
invariant { !s = sum a i k }
s := !s + a[k]
done;
!s
end
(** {2 Additional lemmas on [sum]}
needed in the remaining code *)
module ExtraLemmas
use array.Array
use import ArraySum
(** summation in adjacent intervals *)
lemma sum_concat : forall a:array int, i j k:int.
0 <= i <= j <= k <= a.length ->
sum a i k = sum a i j + sum a j k
(** Frame lemma for [sum], that is [sum a i j] depends only
of values of [a[i..j-1]] *)
lemma sum_frame : forall a1 a2 : array int, i j : int.
0 <= i <= j ->
j <= a1.length ->
j <= a2.length ->
(forall k : int. i <= k < j -> a1[k] = a2[k]) ->
sum a1 i j = sum a2 i j
(** Updated lemma for [sum]: how does [sum a i j] changes when
[a[k]] is changed for some [k] in [[i..j-1]] *)
lemma sum_update : forall a:array int, i v l h:int.
0 <= l <= i < h <= a.length ->
sum (a[i<-v]) l h = sum a l h + v - a[i]
end
(** {2 Algorithm 2: using a cumulative array}
creation of cumulative array is linear
query is in constant time
array update is linear
*)
module CumulativeArray
use array.Array
use import ArraySum
use ExtraLemmas
predicate is_cumulative_array_for (c:array int) (a:array int) =
c.length = a.length + 1 /\
forall i. 0 <= i < c.length -> c[i] = sum a 0 i
(** [create a] builds the cumulative array associated with [a]. *)
let create (a:array int) : array int
ensures { is_cumulative_array_for result a }
= let l = a.length in
let s = Array.make (l+1) 0 in
for i=1 to l do
invariant { forall k. 0 <= k < i -> s[k] = sum a 0 k }
s[i] <- s[i-1] + a[i-1]
done;
s
(** [query c i j a] returns the sum of elements in [a] between
index [i] inclusive and index [j] exclusive, in constant time *)
let query (c:array int) (i j:int) (ghost a:array int): int
requires { is_cumulative_array_for c a }
requires { 0 <= i <= j < c.length }
ensures { result = sum a i j }
= c[j] - c[i]
(** [update c i v a] updates cell [a[i]] to value [v] and updates
the cumulative array [c] accordingly *)
let update (c:array int) (i:int) (v:int) (ghost a:array int) : unit
requires { is_cumulative_array_for c a }
requires { 0 <= i < a.length }
writes { c, a }
ensures { is_cumulative_array_for c a }
ensures { a[i] = v }
ensures { forall k. 0 <= k < a.length /\ k <> i ->
a[k] = (old a)[k] }
= 'Init:
let incr = v - c[i+1] + c[i] in
a[i] <- v;
for j=i+1 to c.length-1 do
invariant { forall k. j <= k < c.length -> c[k] = sum a 0 k - incr }
invariant { forall k. 0 <= k < j -> c[k] = sum a 0 k }
c[j] <- c[j] + incr
done
end
(** {2 Algorithm 3: using a cumulative tree}
creation is linear
query is logarithmic
update is logarithmic
*)
module CumulativeTree
use array.Array
use import ArraySum
use ExtraLemmas
use import int.ComputerDivision
type indexes =
{ low : int;
high : int;
isum : int;
}
type tree = Leaf indexes | Node indexes tree tree
function indexes (t:tree) : indexes =
match t with
| Leaf ind -> ind
| Node ind _ _ -> ind
end
predicate is_indexes_for (ind:indexes) (a:array int) (i j:int) =
ind.low = i /\ ind.high = j /\
0 <= i < j <= a.length /\
ind.isum = sum a i j
predicate is_tree_for (t:tree) (a:array int) (i j:int) =
match t with
| Leaf ind ->
is_indexes_for ind a i j /\ j = i+1
| Node ind l r ->
is_indexes_for ind a i j /\
i = l.indexes.low /\ j = r.indexes.high /\
let m = l.indexes.high in
m = r.indexes.low /\
i < m < j /\ m = div (i+j) 2 /\
is_tree_for l a i m /\
is_tree_for r a m j
end
(** {3 creation of cumulative tree} *)