Commit 86abf6c9 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into itp

parents bcb1525f 89c3adc3
François Bobot <francois@bobot.eu> <bobot@lri.fr>
François Bobot <francois@bobot.eu> <francois.bobot@cea.fr>
Martin Clochard <martin.clochard@lri.fr> <martin@pc-stagiaire.(none)>
Martin Clochard <martin.clochard@lri.fr> <clochard@MC-MacBook.(none)>
Sylvain Dailler <dailler@adacore.com> <sdailler@hauzar@adacore.com>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <Jean-Christophe.Filliatre@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@gemini.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@balrog.(none)>
Clément Fumex <clement.fumex@inria.fr> <fumex@moloch.lri.fr>
Léon Gondelman <gondelmans@lri.fr> <gondelmans@lri.fr>
Léon Gondelman <gondelmans@lri.fr> <lgondelmann@gmail.com>
Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
David Hauzar <david.hauzar@inria.fr> <hauzar@moloch.lri.fr>
Johannes Kanig <kanig@adacore.com> <johannes.kanig@lri.fr>
Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
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>
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>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
Mário José Parreira Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário José Parreira Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário José Parreira Pereira <mpereira@lri.fr> <mpereira@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@lri.fr>
Asma Tafat-Bouzid <atafat@lri.fr> <atafat@atafat-desktop.(none)>
Piotr Trojanek <piotr.trojanek@altran.com> <piotr.trojanek@gmail.com>
......@@ -88,12 +88,15 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
# 44 Open statement shadows an already defined identifier.
# 45 Open statement shadows an already defined label or constructor.
# 50 Unexpected documentation comment.
# 52 The argument of this constructor should not be matched against a
# constant pattern; the actual value of the argument could change
# in the future.
# - fatal:
# 5 Partially applied function: expression whose result has function
# type and is ignored.
# 48 Implicit elimination of optional arguments.
WARNINGS = A-4-9-41-44-45-50@5@48
WARNINGS = A-4-9-41-44-45-50-52@5@48
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
......@@ -124,8 +127,6 @@ EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TARGET_EMACS = share/emacs/why3.elc
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
###############
......@@ -291,11 +292,7 @@ clean_old_install::
rm -rf $(OCAMLINSTALLLIB)/why3
ifeq ($(EMACS),no)
install_no_local:: clean_old_install
else
install_no_local:: clean_old_install $(TARGET_EMACS)
endif
$(MKDIR_P) $(BINDIR)
$(MKDIR_P) $(LIBDIR)/why3
$(MKDIR_P) $(TOOLDIR)
......@@ -306,7 +303,6 @@ endif
$(MKDIR_P) $(DATADIR)/why3/theories
$(MKDIR_P) $(DATADIR)/why3/modules/mach
$(MKDIR_P) $(DATADIR)/why3/drivers
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) theories/*.why $(DATADIR)/why3/theories
$(INSTALL_DATA) modules/*.mlw $(DATADIR)/why3/modules
$(INSTALL_DATA) modules/mach/*.mlw $(DATADIR)/why3/modules/mach
......@@ -356,16 +352,19 @@ uninstall: clean_old_install
clean_old_install::
rm -f $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
rm -f $(DATADIR)/emacs/site-lisp/why3.elc
endif
install_no_local::
$(MKDIR_P) $(DATADIR)/emacs/site-lisp/
$(INSTALL_DATA) share/emacs/why3.el $(DATADIR)/emacs/site-lisp/why3.el
ifneq ($(EMACS),no)
ifeq (@enable_emacs_compilation@,yes)
$(INSTALL_DATA) share/emacs/why3.elc $(DATADIR)/emacs/site-lisp/why3.elc
endif
ifeq (@enable_emacs_compilation@,yes)
all: share/emacs/why3.elc
endif
##################
# Why3 plugins
......@@ -585,7 +584,7 @@ CPULIM_O := $(addprefix src/server/, $(addsuffix .o, $(CPULIM_MODULES)))
TOOLS = lib/why3server$(EXE) lib/why3cpulimit$(EXE)
byte opt: $(TOOLS)
all: $(TOOLS)
lib/why3server$(EXE): $(SERVER_O)
$(CC) -Wall -o $@ $^
......@@ -593,11 +592,8 @@ lib/why3server$(EXE): $(SERVER_O)
lib/why3cpulimit$(EXE): $(CPULIM_O)
$(CC) -Wall -o $@ $^
%.o: %.c %.h
$(CC) -c -Wall -g -o $@ $<
%.o: %.c
$(CC) -c -Wall -g -o $@ $<
$(CC) -Wall -O -g -o $@ -c $<
install_no_local::
$(MKDIR_P) $(LIBDIR)/why3
......@@ -1083,9 +1079,7 @@ COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
$(SHOW) 'Coqdep $<'
$(HIDE)$(COQDEP) -R lib/coq Why3 $< $(TOTARGET)
opt byte: $(COQVO)
install_local:: $(COQVO) drivers/coq-realizations.aux
all: $(COQVO)
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
......@@ -1108,11 +1102,11 @@ drivers/coq-realizations.aux: Makefile
endif
all: drivers/coq-realizations.aux
install_no_local::
$(INSTALL_DATA) drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
opt byte: drivers/coq-realizations.aux
clean::
rm -f drivers/coq-realizations.aux
......@@ -1170,8 +1164,6 @@ install_no_local::
$(INSTALL_DATA) $(addsuffix .pvs, $(PVSLIBS_FP)) $(LIBDIR)/why3/pvs/floating_point/
$(INSTALL_DATA) drivers/pvs-realizations.aux $(DATADIR)/why3/drivers/
install_local:: drivers/pvs-realizations.aux
update-pvs: bin/why3realize.@OCAMLBEST@ drivers/pvs-realizations.aux
for f in $(PVSLIBS_INT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T int.$$f -o lib/pvs/int/; done
for f in $(PVSLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/pvs-realize.drv -T real.$$f -o lib/pvs/real/; done
......@@ -1190,7 +1182,7 @@ install_no_local::
endif
opt byte: drivers/pvs-realizations.aux
all: drivers/pvs-realizations.aux
clean::
rm -f drivers/pvs-realizations.aux
......@@ -1339,7 +1331,7 @@ $(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.au
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
# all: update-isabelle
clean::
rm -f lib/isabelle/*/*.xml
......@@ -1355,7 +1347,7 @@ install_no_local::
endif
opt byte: drivers/isabelle-realizations.aux
all: drivers/isabelle-realizations.aux
clean::
rm -f drivers/isabelle-realizations.aux
......@@ -2083,7 +2075,7 @@ doc/version.tex: doc/version.tex.in config.status
config.status: configure
./config.status --recheck
opt byte: lib/why3/META .merlin
all: lib/why3/META .merlin
lib/why3/META: lib/why3/META.in config.status
./config.status chmod --file $@
......
......@@ -127,6 +127,12 @@ AC_ARG_ENABLE(profiling,
AS_HELP_STRING([--enable-profiling], [enable profiling]),,
enable_profiling=no)
# Emacs compilation
AC_ARG_ENABLE(emacs-compilation,
AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
enable_emacs_compilation=yes)
# either relocation or local, not both
if test "$enable_relocation" = yes ; then
if test "$enable_local" = yes ; then
......@@ -348,7 +354,13 @@ if test "$enable_html_doc" = yes ; then
fi
# checking for emacs
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$enable_emacs_compilation" = yes ; then
AC_CHECK_PROG(EMACS,emacs,emacs,no)
if test "$EMACS" = no ; then
enable_emacs_compilation=no
AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
fi
fi
# checking for Zarith
if test "$enable_zarith" = yes; then
......@@ -786,6 +798,8 @@ AC_SUBST(enable_html_doc)
AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)
AC_SUBST(enable_emacs_compilation)
AC_SUBST(EMACS)
AC_SUBST(enable_frama_c)
......
......@@ -216,7 +216,8 @@ The provers can give the following output:
\label{sec:proveoptions}
\begin{description}
\item[\texttt{-{}-get-ce}] activates the generation of a potential counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-get-ce}] activates the generation of a potential
counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
\textsl{s} as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
......@@ -470,7 +471,125 @@ are grouped together under several tabs.
decision by clicking on it.
\end{description}
% \subsection{Displaying Counterexamples}
\subsection{Displaying Counterexamples}
When the selected prover finds (counterexample) model, it is possible to
display parts of this model in the terms of the original Why3 input.
Currently, this is supported for CVC4 prover version 1.5 and newer.
To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File -/> Preferences -/> get
counter-example.
After running the prover and clicking on the prover result in, the
counterexample can be displayed in the tab
Counter-example.
The counterexample is displayed with the original Why3 code in comments.
Counterexample values for Why3 source code elements at given line are
displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elemets that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a
Why3 theory with some terms annotated with the \texttt{model} label and the
generated counterexample in comments:
\begin{whycode}
theory T
use import int.Int
goal g_no_lab_ex : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
("model" "model_trace:x+3<=50" x + 3 <= 50)
goal computation_ex : forall x1 "model" x2 "model" x3 "model" .
(* x1 = 1; x2 = 1; x3 = 1 *)
("model" "model_trace: x1 + 1 = 2" x1 + 1 = 2) ->
(* x1 + 1 = 2 = true *)
("model" x2 + 1 = 2) ->
(* (= (+ x2 1) 2) = true *)
("model" x3 + 1 = 2) ->
(* (= (+ x3 1) 2) = true *)
("model" x1 + x2 + x3 = 5)
(* (= (+ (+ x1 x2) x3) 5) = false *)
\end{whycode}
To display counterexample values in assertions the term being asserted must be
labeled with the label \texttt{"model\_vc"}. To display counterexample values
in postconditions, the term in the postcondition must be labeled with the
label \texttt{"model\_vc\_post"}.
The following example shows a counterexample of a function with postcondition:
\begin{whycode}
let incr_ex ( x "model" : ref int ) (y "model" : ref int): unit
(* x = -2; y = -2 *)
ensures { !x = old !x + 2 + !y }
=
y := !y + 1;
(* y = -1 *)
x := !x + 1;
(* x = -1 *)
x := !x + 1
(* x = 0 *)
\end{whycode}
It is also possible to rename counterexample elements using the lable
\texttt{"model\_trace:"}. The following example shows the use of renaming a
counterexample element in order to print the counterexample in infix notation
instead of default prefix notation:
\begin{whycode}
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
(* x = 48; (<= 42 x) = true *)
("model" "model_trace:x+3<=50" x + 3 <= 50)
(* x+3<=50 = false *)
\end{whycode}
Renaming counterexample elements is in particular useful when Why3 is used as
intermediate language and to show names of counterexample elements in the
source language instead of showing names of Why3 elements.
Note that if the counterexample element is of a record type, it is also
possible to rename names of the record fields by putting the label
\texttt{model\_trace:} to definitions of record fields. For example:
\begin{whycode}
type r = {f "model_trace:.F" :int; g "model_trace:G" :bool}
\end{whycode}
When a prover is queried for a counterexample value of a term of an abstract
type=, an internal representation of the value is get. To get the concrete
representation, the term must be marked with the label
\texttt{"model\_projected"} and a projection function from the abstract type
to a concrete type must be defined, marked as a projection using the meta
\texttt{"model\_projection"}, and inlining of this function must be disabled
using the meta \texttt{"inline : no"}. The following example shows a
counterexample of an abstract value:
\begin{whycode}
theory A
use import int.Int
type byte
function to_rep byte : int
predicate in_range (x : int) = -128 <= x <= 127
axiom range_axiom : forall x:byte.
in_range (to_rep x)
meta "model_projection" function to_rep
meta "inline : no" function to_rep
goal abstr : forall x "model_projected" :byte. to_rep x >= 42 -> to_rep x
+ 3 <= 50
(* x = 48 *)
\end{whycode}
More examples of using counterexample feature of Why3 can be found in the file
examples/tests/cvc4-models.mlw and examples/tests/cvc4-models.mlw.
More information how counterexamples in Why3 works can be found
in~\cite{sefm16}.
%
% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
%
......
......@@ -232,3 +232,21 @@ Claude March\'e and Andrei Paskevich},
year = {2007}
}
@inproceedings{sefm16,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
booktitle = {Proceedings of the 8th Conference on Real Numbers and
Computers},
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
topics = {team},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
}
\ No newline at end of file
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.4pl6" timelimit="60" steplimit="0" memlimit="1000"/>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......
module Bug
use HighOrd
type foo = { a: unit -> unit ; b : unit }
constant bar : foo = {
a = \_. () ;
b = ()
}
end
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../floats.why" expanded="true">
......
......@@ -3,7 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.2.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="1" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="3" name="Spass" version="3.7" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
......
......@@ -6,7 +6,7 @@
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.1.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
......
(** {1 Euler Project, problem11}
In the 20×20 grid below, four numbers along a diagonal line have been marked in red.
{h <Pre>
08 02 22 97 38 15 00 40 00 75 04 05 07 78 52 12 50 77 91 08
49 49 99 40 17 81 18 57 60 87 17 40 98 43 69 48 04 56 62 00
81 49 31 73 55 79 14 29 93 71 40 67 53 88 30 03 49 13 36 65
52 70 95 23 04 60 11 42 69 24 68 56 01 32 56 71 37 02 36 91
22 31 16 71 51 67 63 89 41 92 36 54 22 40 40 28 66 33 13 80
24 47 32 60 99 03 45 02 44 75 33 53 78 36 84 20 35 17 12 50
32 98 81 28 64 23 67 10 26 38 40 67 59 54 70 66 18 38 64 70
67 26 20 68 02 62 12 20 95 63 94 39 63 08 40 91 66 49 94 21
24 55 58 05 66 73 99 26 97 17 78 78 96 83 14 88 34 89 63 72
21 36 23 09 75 00 76 44 20 45 35 14 00 61 33 97 34 31 33 95
78 17 53 28 22 75 31 67 15 94 03 80 04 62 16 14 09 53 56 92
16 39 05 42 96 35 31 47 55 58 88 24 00 17 54 24 36 29 85 57
86 56 00 48 35 71 89 07 05 44 44 37 44 60 21 58 51 54 17 58
19 80 81 68 05 94 47 69 28 73 92 13 86 52 17 77 04 89 55 40
04 52 08 83 97 35 99 16 07 97 57 32 16 26 26 79 33 27 98 66
88 36 68 87 57 62 20 72 03 46 33 67 46 55 12 32 63 93 53 69
04 42 16 73 38 25 39 11 24 94 72 18 08 46 29 32 40 62 76 36
20 69 36 41 72 30 23 88 34 62 99 69 82 67 59 85 74 04 36 16
20 73 35 29 78 31 90 01 74 31 49 71 48 86 81 16 23 57 05 54
01 70 54 71 83 51 54 69 16 92 33 48 61 43 52 01 89 19 67 48
</Pre> }
The product of these numbers is 26 × 63 × 78 × 14 = 1788696.
What is the greatest product of four adjacent numbers in the same direction (up, down, left, right, or diagonally) in the 20×20 grid?
*)
module ProductFour
use import int.Int
use import ref.Ref
use import matrix.Matrix
use import option.Option
(** Direction of the product checked *)
type direction =
| Left_bottom
| Right_bottom
| Bottom
| Right
(** Math functions about the result of a product. Incomplete product generate None *)
function left_diag (m: matrix int) (i: int) (j: int) : option int =
if (i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3) then
Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3))))
else
None
function right_diag (m: matrix int) (i: int) (j: int) : option int =
if (i < m.rows - 3 /\ i >= 0 /\ j < m.columns - 3 /\ j >= 0) then
Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3))))
else
None
function line (m: matrix int) (i: int) (j: int) : option int =
if (0 <= j < m.columns /\ i >= 0 /\ i < m.rows - 3) then
Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j))
else
None
function column (m: matrix int) (i: int) (j: int) : option int =
if (0 <= i < m.rows /\ j >= 0 /\ j < m.columns - 3) then
Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3)))
else
None
(** Computational functions for the product in each direction *)
let right_diag_c m i j : option int =
ensures {result = right_diag m i j}
if (i < m.rows - 3 && i >= 0 && j < m.columns - 3 && j >= 0) then
Some (((get m i j) * (get m (i + 1) (j + 1)) * (get m (i + 2) (j + 2)) * (get m (i+3) (j+3))))
else
None
let left_diag_c m i j : option int =
ensures {result = left_diag m i j}
if (i < m.rows && j >= 0 && i >= 3 && j < m.columns - 3) then
Some (((get m i j) * (get m (i - 1) (j + 1)) * (get m (i - 2) (j + 2)) * (get m (i-3) (j+3))))
else
None
let line_c m i j : option int =
ensures {result = line m i j}
if (0 <= j && j < m.columns && i >= 0 && i < m.rows - 3) then
Some ((get m i j) * (get m (i+1) j) * (get m (i+2) j) * (get m (i+3) j))
else
None
let column_c m i j : option int =
ensures {result = column m i j}
if (0 <= i && i < m.rows && j >= 0 && j < m.columns - 3) then
Some ((get m i j) * (get m i (j+1)) * (get m i (j+2)) * (get m i (j + 3)))
else
None
(* function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int = *)
(* match d with *)
(* | Left_bottom -> left_diag m i j *)
(* | Right_bottom -> right_diag m i j *)
(* | Bottom -> column m i j *)
(* | Right -> line m i j *)
(* end *)
(* TODO Failed attempt at pattern matching above. Combination of mathematical product result functions *)
function compute4 (m: matrix int) (i: int) (j: int) (d: direction) : option int =
if (d = Left_bottom) then left_diag m i j
else if (d = Right_bottom) then right_diag m i j
else if (d = Bottom) then column m i j
else if (d = Right) then line m i j
else None
(** A product is_valid if each elements of the product is in the matrix *)
(* predicate is_valid (m: matrix int) (i: int) (j: int) (d: direction) = *)
(* match d with *)
(* | Left_bottom -> i < m.rows /\ j >= 0 /\ i >= 3 /\ j < m.columns - 3 *)
(* | Right_bottom -> i >= 0 /\ j >= 0 /\ i < m.rows - 3 /\ j < m.columns - 3 *)
(* | Bottom -> 0 <= i /\ i < m.rows /\ j >= 0 /\ j < m.columns - 3 *)
(* | Right -> 0 <= j /\ j < m.columns /\ i >= 0 /\ i < m.rows - 3 *)
(* end *)
(** Return the maximum product of 4 for matrix m *)
let find_max (m: matrix int) =
requires {m.rows > 4 /\ m.columns > 4}
ensures {forall i j d. match (compute4 m i j d) with
| None -> true
| Some v -> v <= result
end}
ensures {exists i j d. Some result = compute4 m i j d}
(** Current max and element of the matrix for which it is attained *)
let cur_max = ref (
match (line_c m 0 0) with
| None -> 0 (* TODO should not happen *)
| Some v -> v
end) in
let cur_i = ref 0 in
let cur_j = ref 0 in
let cur_d = ref Right in
for i = 0 to (m.rows - 1) do
(* Cur_max is greater than each product already seen *)
invariant { forall i' j' d. (0 <= i' < i /\ 0 <= j' < m.columns) ->
match (compute4 m i' j' d) with
| None -> true
| Some v -> v <= !cur_max
end}
(* cur_max is actually the product at (cur_i, cur_j, cur_d) *)
invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d}
for j = 0 to (m.columns - 1) do
(* cur_max is actually the product at (cur_i, cur_j, cur_d) *)
invariant {Some !cur_max = compute4 m !cur_i !cur_j !cur_d}
(* Cur_max is greater than each product already seen *)
invariant { forall i' j' d. ((i' = i /\ 0 <= j' /\ j' < j) \/ (0 <= i' < i /\ 0 <= j' < m.columns)) ->
match (compute4 m i' j' d) with
| None -> true
| Some v -> v <= !cur_max
end}
(* Computation of the product for each direction *)
match (left_diag_c m i j) with
| None -> ()
| Some v ->