Re: [Why3-club] Printing in WhyML Code?

Le 19/02/2021 à 22:14, Frank Pfenning a écrit : Thanks, that's indeed helpful. Where can I find documentation (or source) on libraries io.* and perhaps other system-relevant libraries that do not appear on http://why3.lri.fr/stdlib/ ? Well, in principle all the standard packages should be

Re: [Why3-club] Printing in WhyML Code?

Le 19/02/2021 à 17:19, Claude Marche a écrit : ```hello.mlw let test () =   print_string "Hello Why3 World";   print_newline () ``` With `use io.StdIO` as first line, of course - Claude ___ Why3-club mailing list Why3-club@lists.gforg

Re: [Why3-club] Printing in WhyML Code?

Le 17/02/2021 à 13:44, Frank Pfenning a écrit : We are using WhyML/Why3 in a course on Bug Catching at CMU, and one of the students asked if it was possible to insert print statements into their code.  Presumably, they'd want the interpreter (why3 execute) to show them the value of variables

Re: [Why3-club] function.mlw

Le 23/09/2020 à 14:36, Guillaume Melquiond a écrit : Since lemmas cannot be referred to, this indeed seems like an artificial limitation . Not true : you can do "apply H", "rewrite H" and these kinds of things in the interactive theorem proving interface of Why3, without forgetting the

Re: [Why3-club] Problems with Z3 and CVC4

sformation "compute_specified" before calling the provers See http://why3.lri.fr/doc/technical.html - Claude Le 28/04/2020 à 12:14, Claude Marche a écrit : Adding an extra predicate adds a very small amount of input for the prover and sometimes it is enough to turn proved VCs into unproved ones.

Re: [Why3-club] Problems with Z3 and CVC4

Le 27/04/2020 à 15:47, margarita.capretto a écrit : Dear colleagues, We have another issue while using CVC4 to prove some simple code in WhyML. For example, for the following code use int.Int use list.ListRich use string.OCaml predicate post (n: int) (result: int) = result = 3*n let f (n:

Re: [Why3-club] Problems with Z3 and CVC4

Hi Margarita, sorry for the late answer Le 20/04/2020 à 17:58, margarita.capretto a écrit : Dear colleagues, My name is Margarita Capretto and I am doing research with prof. Cesar Sanchez at the IMDEA Software Institute. We are using Why3 (and in particular WhyML) for deductive software

Re: [Why3-club] New release Why3 1.3.1

Le 24/03/2020 à 21:47, Guillaume Melquiond a écrit : Le 24/03/2020 à 21:42, Julia Lawall a écrit : * fixed conflicting symbols for CVC4 1.7 I'm not sure what this change is, but after doing a pull of the latest version, I still have to remove the --strings-exp option to get cvc4 to

Re: [Why3-club] cvc4

Hello, Le 18/03/2020 à 12:31, Julia Lawall a écrit : But the unconditional (get-info :reason-unknown) doesn't look ideal. Agreed. Unfortunately, to make it conditional, Why3 would have to interact with the SMT solvers, that is, write on stdin, read on stdout, write on stdin, read on stdout,

[Why3-club] Call for participation JFLA 2020

(This message is intentionally written in French) *Merci de faire circuler : premier appel à communications * JFLA'2020 (http://jfla.inria.fr/jfla2020.html) Journées Francophones des Langages Applicatifs Gruissan - du 29 janvier au 1 février 2020 Les

Re: [Why3-club] Mixing integers and reals

Hello, I have no simple answer on that, but a few suggestions Did you try CVC4 or Z3? If yes do you get similar behavior? I guess one should investigate if provers like Alt-Ergo/CVC4/Z3 have a built-in support for conversion from integers to reals. If yes, then one should check that Why3

Re: [Why3-club] lemma usage

Le 03/10/2019 à 09:06, Julia Lawall a écrit : lemma valid_cont_remove_from_current : forall oldcrs crs:cores, core co:int, t:thread, c:cont. valid_core oldcrs core -> valid_cont oldcrs core c -> core <> co -> cont_thread c <> Some t -> amem t oldcrs.current co ->

Re: [Why3-club] lemma usage

Le 03/10/2019 à 09:02, Julia Lawall a écrit : On Thu, 3 Oct 2019, Claude Marche wrote: Notice that if your initial goal is to apply the lemma at the right place with the right instantiation, then a "let lemma" is not necessary, a "let ghost" is enough. An

Re: [Why3-club] lemma usage

Le 03/10/2019 à 08:57, Julia Lawall a écrit : If the quantified variables are always the same, you can move them from the arguments to the postcondition of the lemma function. So take the foralls and all of the requires and put them into a big implication in the ensures? A priori I would

Re: [Why3-club] lemma usage

Hi club, Le 03/10/2019 à 08:26, Guillaume Melquiond a écrit : Le 02/10/2019 à 15:16, Julia Lawall a écrit : Hmm, in looking further, I have the impression that I can't make a let lemma because the lemma needs to be universally quantified over some variables. If the quantified variables

Re: [Why3-club] problems installing why3 from git repository

Hi Virginia, Just to say that we had the same problem very recently, that seems related to the computation of dependencies after the parser is modified. I suggest you try you update again your git to the current master branch and retry to compile. In case it happens again, a fix could be

Re: [Why3-club] build from sources

Hello, For the record, if others have the same issue: rm lib/why3/why3extract.cmi should solve the problem - Claude Le 03/09/2019 à 08:07, Guillaume Melquiond a écrit : Le 03/09/2019 à 07:54, Julia Lawall a écrit : With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the

Re: [Why3-club] return type of let lemma

Hello Marc, Yes it is an intentional additional feature. As explained briefly by Francois, a function of profile let lemma f (x1:t1) .. (x_k:t_k) : t requires {P} ensures {Q} is turned into the hypothesis forall x1:t_1,..,x_k:t_k. P -> exists result:t. Q By the way, I am always

Re: [Why3-club] Set equality

Hi Why3 Club Le 10/05/2019 à 08:30, Guillaume Melquiond a écrit : I would expect Why3 to use Please note that such a sentence is meaningless: Why3 is not a prover per se, it calls external provers. If you ask "I would expect Alt-Ergo/CVC4/Z3 to use ..." then see Guillaume answer. An

Re: [Why3-club] Higher order function

In older versions of Why3 you probably needed to add `use import HighOrd` - Claude Le 07/05/2019 à 09:32, Guillaume Melquiond a écrit : Le 07/05/2019 à 08:47, Aurélie Hurault a écrit : Hello, I'd like to use higher order functions in Why3, but I have trouble. Which version of Why3 are you

Re: [Why3-club] concurrency

Hello Julia, I'm not sure how to help, but I wonder: how many provers you asked Why3 to run in parallel? I suggest you should not use 48, because you will have no remaining cores for the main Why3 process, and other processes of your system. - Claude Le 18/04/2019 à 11:35, Julia Lawall a

Re: [Why3-club] Why3-club Digest, Vol 95, Issue 7

Le 29/03/2019 à 14:56, Sandrine Blazy a écrit : Dear Claude, Le 15 nov. 2018 à 12:01, why3-club-requ...@lists.gforge.inria.fr a écrit : Since Why3 1.0 we wanted to disencourage users to intentionally choose a particular prover to discharge a

Re: [Why3-club] Questions about the why3 ide

Le 29/03/2019 à 09:39, Julia Lawall a écrit : The editor recently introduced in Why3 provides a great improvement to the user experience. Thanks a lot. Thanks for your positive feedback! I use this a lot as well. I miss the ability to search, particularly in the task view. julia I

Re: [Why3-club] Questions about the why3 ide

Hello, Le 28/03/2019 à 16:38, Delphine Demange a écrit : Hi, The editor recently introduced in Why3 provides a great improvement to the user experience. Thanks a lot. Thanks for your positive feedback! I'm running the Why3 platform, version 1.1.0. I'd like to know whether it is possible

[Why3-club] Call for participation: Frama-C & SPARK Day 2019, June 3rd, Paris

*Frama-C & SPARK Day 2019 : Formal Analysis and Proof for Programs in C and Ada* Date: Monday June 3rd, 2019 Location: Paris, La Fabrique Événementielle, 52 ter Rue des Vinaigriers, 75010 This one-day workshop aims at gathering both academic and industrial users of the

Re: [Why3-club] plans about why/krakatoa ?

Hello, To give an answer to this question: the maintenance of the why package, that was providing the Why3 front-ends for Java (Krakatoa) and C (the Jessie plug-in of Frama-C) depends on shallow human resources that are not sufficient for the upgrade to Why3 1.xx There are currently

Re: [Why3-club] strategy definitions in the config file

Sorry for the late answer. Please look at the manual http://why3.lri.fr/doc/technical.html#sec137 for a description of the language of proof strategies. As shown by Mario's answer, the "t" instruction requires both a transformation name and a label. You did not give any label. The newlines

Re: [Why3-club] inlining functions or explicit predicates

Dear JJ, As you remark, Why3 0.88 is now quite outdated and my answer may not be very accurate. As far as I remember, the former "Inline" button was applying the transformation "inline_goal" which has the effect of inlining the defined function symbols appearing in an outermost position in

Re: [Why3-club] replacement of gtk2?

Hello Ralf, This is not Why3 specific: did you ask the same questions to the Caml mailing list? I would be interested to know the answers... In other words: are there any plans for a lablgtk3? Concerning Why3: there is indeed a prototype (in a very early stage) for a graphical interface inside

Re: [Why3-club] Why3 IDE

Le 19/10/2016 à 19:37, Per Lindgren a écrit : > Dear Claude > > Thanks for your prompt answer. I will look into this. > > The version I’ve been working with is the one checked out through > opam (0.87.2). Is this the same version as the master branch, or? No it is not. the git master branch

[Why3-club] New release Why3 0.86

A new release of Why3, version 0.86, is available from the Web page http://why3.lri.fr. The OPAM package for this version of Why3 is also available. There is no major change in this release. It mainly provides support for new provers or new versions of provers, and a few new theories in the

Re: [Why3-club] Krakatoa in batch mode

Hi, You can't do that with a single invocation of krakatoa. If it is really needed, it can be done in several steps: krakatoa -gen-only File.java jessie File.jc -locs File.jloc -why3ml -why3-opt prove -P alt-ergo -a split_goal_wp make -f File.makefile why3ml Let me say once more that NOT

Re: [Why3-club] New release Why3 0.85

Fixed. Thanks for reporting the mistake. - Claude On 09/17/2014 01:21 PM, Jean-Jacques Levy wrote: Claude, it looks that the web page refers to the .84 release !!! -JJ- Le 17 sept. 2014 à 11:22, Claude Marché claude.mar...@inria.fr a écrit : A new release of Why3, version

Re: [Why3-club] logical check for alias detection

, -JJ- Le 15 juin 2014 à 13:39, Claude Marche claude.mar...@inria.fr a écrit : On 06/15/2014 05:51 AM, Jean-Jacques Levy wrote: Dear Why3-Friends, is there a way of calling why3 with alias detector off ? I’d like a adhoc test for alias detection. For instance I have a list of records

Re: [Why3-club] logical check for alias detection

On 06/15/2014 05:51 AM, Jean-Jacques Levy wrote: Dear Why3-Friends, is there a way of calling why3 with alias detector off ? I’d like a adhoc test for alias detection. For instance I have a list of records, detected as potential aliases by Why3, but if I have an invariant stating that

Re: [Why3-club] why3/jessie doesn't build with ocaml 4.01 ?

Marino wrote: On 6/4/2014 16:42, Claude Marche wrote: Hi John, 1) If there is a Why3 package in FreeBSD, I suggest it should correspond to Why3 releases, that is, currently, version 0.83 2) If there are both a why3 package and a SPARK2014 package, I recommend to keep them completely independent from

Re: [Why3-club] why3/jessie doesn't build with ocaml 4.01 ?

On 06/05/2014 03:23 PM, John Marino wrote: Everyone wins. I'm not sure but never mind. At least, could you please name your package differently? e.g spark-why3-support or anything similar, representative of its use, and not something about licencing. - Claude

[Why3-club] New release Why3 0.83

A new release of Why3, version 0.83, is available from the Web page http://why3.lri.fr. A detailed list of changes is given below. - Claude, for the Why3 team syntax o extra semicolons are now allowed at end of blocks o new clause diverges. Loops and recursive calls not annotated with

Re: [Why3-club] how to import a theory ?

Hi Sandrine, By default, the loadpath where Why3 searches for theories and modules does not contain ., so you should inkove why3 with option -L . if some theories to import belong to the current directory. . can also be added by hand in the field loadpath of the ~/.why3.conf configuration