Le 19/02/2019 à 16:02, Jean-Jacques Levy a écrit :
Dear Claude,
(* me again *) I did not notice the appset module.. oh so thanks, I’ll try to
use it. But seems to be many sets:
Fset, appset, impset….
See http://why3.lri.fr/stdlib/
set.Set: theory of mathematical sets
set.Fset: theory
Hello JJ,
Short answer: with Why3 1.x you should use one of the modules
appset.Appset or impset.Impset to program with finite sets (depending on
whether you want a mutable data structure or not). More precisely you
should clone one of these, giving the value of type 'elt', in a very
similar
Hi Claire,
Le 31/01/2019 à 14:56, Claire Dross a écrit :
Hi Why3 team,
while working on the port of SPARK to the current master of why3, I
noticed that we have a difference between our current driver for smtlib
and the driver from why3 master. In gnatwhy3, we have some mappings, in
Hello,
The easiest way to achieve this is to add, at the end of the module that
needs a lemma "L" only internally, the declaration
See attached file for example
meta remove_prop lemma L
Hope this helps,
Le 04/01/2019 à 16:48, Julia Lawall a écrit :
Is it possible to make a lemma only
Since Why3 1.0, there is no polymorphic equality in programs. Hence
there is no symbol (=) for type cell in your code, but only the equality
for type int.
The standard workaround is to declare such an equality function as
val (=) (x y:cell) : bool
ensures { result <-> x=y }
of course one
Problem with remaining data from older version of Why3
mv ~/.why3.conf ~/.why3.conf.saved
why3 config --detect
Hope this helps,
- Claude
Le 17/09/2018 à 13:00, Sara Houhou a écrit :
Hello,
Thanks a lot, but I am always blocked by this message when I want to
test the first example:
why3
[Feel free to redistribute this announcement/Apologizes for multiple
copies]
The Joint Laboratory ProofInUse (https://www.adacore.com/proofinuse)
hires an experienced R engineer (M/F) in the domain of Formal Methods
for Software Engineering:
The teaching committee of FME association is collecting all courses on
formal methods, to make them easily searchable/available for teachers
and students.
If you are giving a course on formal methods (in particular if you use
Why3 but not only ;-)) I strongly encourages you to take 2
Thanks David for sharing your experience.
I don't know what is the overall goal of Gian Pietro, but there's a good
chance that producing a text file would be a good approach.
- Claude
Le 08/05/2018 à 22:21, David MENTRÉ a écrit :
Hello,
Le 2018-05-08 à 18:58, Gian Pietro Farina a écrit :
Le 08/05/2018 à 18:58, Gian Pietro Farina a écrit :
Hello,
Sorry for bothering, I am still having troubles in building tasks with
formulas including expressions of the array theory.
I attach a minimal "non working" example.
please next time send a file that is self-contained
Could you
t understand how to do things in ocaml.
Cheers,
GP
On Wed, May 2, 2018 at 5:37 AM, Claude Marché <claude.mar...@inria.fr
<mailto:claude.mar...@inria.fr>> wrote:
Hello,
I guess you already read the chapter 4 of the manual
(http://why3.lri.fr/doc/api.htm
Hello,
I guess you already read the chapter 4 of the manual
(http://why3.lri.fr/doc/api.html#sec30). The importation of modules and
the manipulation of programs is not documented yet, but you can find
some examples of use in the directory examples/use_api of the
distribution: files mlw.ml
lot, for your help!
Abhishek
On Thu, Apr 5, 2018 at 4:49 PM, Claude Marché <claude.mar...@inria.fr
<mailto:claude.mar...@inria.fr>> wrote:
Hello,
Did you try to carefully follow the section
http://why3.lri.fr/doc/api.html#sec30
<http://why3.lri.fr/doc/api.html#sec
.conf file and search for the
"loadpath" items in the [main] section.
If the path above appear there, then remove it.
Alternatively, if you're not afraid of losing specific settings of your
Why3 config, then just remove .why3.conf and rerun
why3 config --detect
- Claude
--
Claude Marché
Why3ide again, you should see you former Coq proof.
If that works on one machine, this should work on the other, if the
directory with the .xml file and the .v file is put under git.
- Claude
PS: I don't think the "mark as obsolete" operation is required, "edit"
will notice if
hy3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http
ves the goal.
Depending on your initial problem, you should consider translating "0 <=
k <= 3 " into "k=0 \/ k=1 \/ k=2 \/ k=3"
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France
of make (fl1) are attached.
>
> thanks,
> julia
>
>
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché
Denis * *Cousineau*, Ph.D
> デニ クズノ
> Researcher
> Formal Methods: Theory, Methodology and Tools
> Information and Network Systems (INS) Team
> Communication & Information Systems (CIS) Division
> *Mitsubishi Electric R Centre Europe* (MERCE)
> Tel: +33(0)2 23 45
w if there is one for Zarith.
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
_
://jobs.inria.fr/public/classic/en/offres/2018-00228
Do not hesitate to forward this email to any appropriate candidates or
mailing lists.
Best regards,
- Claude Marché
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Uni
> Thanks in advance.
> --
> Yannick Moy, Senior Software Engineer, AdaCore
>
>
>
>
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché
tly, breaking the abstraction, I
> can see that using the polymorphic comparison/hash functions, all will
> be fine... but having explicit eq/compare/hash functions for the
> prover_call type would allow me not to rely on breaking the Why3 API
> abstraction.
Good point, we should add them in the
_______
>> Why3-club mailing list
>> Why3-club@lists.gforge.inria.fr
>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gfo
have
> taken into account.
>
>
>
> Regards
>
>
>
> Jens
>
>
>
>
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
--
Claude Marché
the theories of the
standard library. (We should do it for all of them, it is only a matter
of time available...)
Hope this helps,
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.l
gt; The problem disappears if I remove the invariant of `lit`. Is this a bug
> or a feature ? Is there a way I can specify type invariants for
> immutable records.
>
> Best,
> Jonathan Laurent
>
>
> ___
> Why3-club mailing list
>
lub@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www
sion may diverge, which is not stated in the
> specification
You should add the clause "diverges" in the contracts of your
non-terminating functions
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 65
nd is to compile
using
./configure --disable-zip
make
which would disable compression of shapes.
> Thanks for any help, -JJ-
Don't know if it helps, but I hope
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université
Le 16/11/2016 à 10:08, Claude Marché a écrit :
> This addition is due to Martin Clochard, a paper explaining that should
> appear very soon (in French first, sorry for non-french speaking
> user...)
For info, the paper in question is there :
https://hal.inria.fr/hal-01404935
--
Clau
code.
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex|
___
Why3-club mailing
ctly because
it requires reasoning by induction on the list.
Home work:
* prove the goal using the 'induction_ty_lex' transformation
* prove the goal using a lemma function
* prove the goal using an interactive prover of your choice (Coq,
Isabelle/HOL, PVS)
Have a nice day !
- Claude
--
C
may consider start a fresh installation with a newer
version of OCaml :
opam switch 4.02.3
opam install conf-gmp conf-gtksourceview why3
(compilation of Coq will take some time, sorry about that)
- Claude
Le 02/03/2016 14:40, Pablo M. S. Farias a écrit :
> Dear Claude Marché,
>
> I
1: 63283 Segmentation fault: 11 WHY3CONFIG= coqc -opt -I
lib/coq-tactic/ lib/coq-tactic/Why3.v
# make: *** [src/coq-tactic/.why3-vo-opt] Error 139
'opam install why' failed.
--
Claude Marché | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France |
Université
definitions
provers
o fixed wrong warning when detecting Isabelle2014
--
Claude Marché | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex
files with links to the
proof obligations generated for
each prover ?
- Mohamed.
--
Claude Marché | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France |
Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex
/~marche/MPRI-2-36-1/install.html to
install why3 but when I try to run it, Linux says why3ide cannot be
found. I was wondering if you could help me solving this problem. I
thank you in advance.Best regards, Fabio Bucciarelli
--
Claude Marché | tel: +33 1 72 92 59 69
INRIA
39 matches
Mail list logo
