Dear Why3-Folks,
Happy New Year! Let 2014 be much fruitful for Why3!
I run Why3 version 0.82 and E-prover 1.6. Following assertions are proved by
E-prover !! Which looks to me (and Chen Ran) quite abnormal. It is not proved
by others provers,
Do we miss anything ? (BTW, I asked -- in
Jean-Christophe and Why3 Friends,
I think that Coq will not bring anything.
What looks weird to me is that inductive def of 'permut_sub'. From beginning
I'm not pleased with it. The base case 'permut_refl' implies that one can use
'permut_sub' only for in-situ permutations. It looks
Dear Why3 Friends,
recently ‘why3ide’ got new behavior on my Macbook Air. Fonts to the left get
very large. And I cannot find way to reduce their size. Maybe it’s X-server
which changed. Don’t know that happened. Anyone with same problem ?
Furthermore, I cannot remember way to set preferences
Many thanks. So your advice is to use the development version. -JJ-
Le 11 mars 2014 à 15:56, Jean-Christophe Filliâtre
jean-christophe.fillia...@lri.fr a écrit :
Dear Jean-Jacques,
Le 11/03/2014 07:33, Jean-Jacques Levy a écrit :
following problem of early February, is there a fix
Dear Why3 Friends!
from time to time, I met difficulties in making a constructive Coq proof
corresponding to a Why3 goal. Has anybody met same problem ?
Must of time it comes from translation of Why3 predicates into Prop's, instead
of a Coq predicate (with truth values). Then it’s hard to
Guillaume,
many thanks for your answer. But:
Le 9 mai 2014 à 16:22, Guillaume Melquiond guillaume.melqui...@inria.fr a
écrit :
2- is it fair to use Classical logic in the Coq stubs translated from Why3
goals/lemmas ?
Yes, it is fair, since the logic of Why3 already assumes it.
In
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 list has never 2 equal elements, there would not be any
But what’s size of that new array ? It looks your array is the full memory map…
+ doing manual memory allocation. Claude, you do not believe in garbage
collectors ?
Cheers, -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
Dear Martin,
I will isolate that problem and let you know asap. But I have a second issue:
When using the Queue module, I'd like have an invariant on the content of the
queue. What is the good way for it ? For instance, let f be a queue, then
making predicates on f.elts seems not working.
let
François, it now does work. Thanks, -JJ-
> Le 26 mai 2016 à 14:40, François Bobot <francois.bo...@cea.fr> a écrit :
>
> On 26/05/2016 14:27, Jean-Jacques Levy wrote:
>> Dear Why3-Friends,
>>
>> running 'why3 0.87.0’ (just installed with opam), I got 2 errors
Dear Why3-Friends,
running 'why3 0.87.0’ (just installed with opam), I got 2 errors:
1- « /usr/local/lib/why3/plugins/dimacs cant’t be loaded » Opam did not install
that plugin at correct location ?! but it worked after linking
/usr/local/lib/why3 to ~/.opam/system/lib/why3 !!
2- glib failed
Hello Friends!
I now always get following message:
> Why3ide callback raised an exception:
> anomaly: Gzip.Error("error during compression »)
when saving Why3 session. I reinstalled all (MacPorts) packages and still get
that message.
I assume it’s when why3ide is producing the
the stack trace coming from IDE is not informative unfortunately
>
> Le 01/02/2017 à 14:30, Jean-Jacques Levy a écrit :
>> File "scc/../scc.mlw", line 249, characters 23-33:
>> warning: this expression may diverge, which is not stated in the
>> specification
>
stack trace coming from IDE is not informative unfortunately
>
> Le 01/02/2017 à 14:30, Jean-Jacques Levy a écrit :
>> File "scc/../scc.mlw", line 249, characters 23-33:
>> warning: this expression may diverge, which is not stated in the
>> specification
>
...
I finally succeeded in compiling and installing why3 0.87.3 with macosx 10.12.3
(without the gzip option). Was not so easy to get macports and opam consistent.
But with double ocaml systems, it has worked out.
(I’m still suspicious with Gzip under that version of macosx)
Thanks Claude for
Dear Why3-Friends,
I tried to use why3 tactic, and failed.
Print LoadPath. —> response:
Logical Path: Physical path:
<>/Users/levy/.opam/4.02.2/lib/why3/coq-tactic
Why3 /Users/levy/.opam/4.02.2/lib/why3/coq
Why3.set
But:
let f (x: int) (ghost y: int) (ghost dy: ref int) = dy := y; x
is no longer applicative programming style.. You have side effect.
-JJ-
> Le 9 nov. 2016 à 15:18, Andrei Paskevich <andrei.paskev...@lri.fr> a écrit :
>
> Dear Jean-Jacques,
>
> On 9 November 2016 a
Dear Why3 Friends,
what is best way of having a ghost component in the results of functions ?
A record with a ghost field as a return value of a function seems accepted by
why3.
type rr = { dx: int; ghost dy : int}
let f (x: int) (ghost y: int) = {dx = x; dy = y}
A tuple with a ghost
Dear Why3 folks,
here is a small termination problem which I cannot solve. Pls help!
Thanks -JJ-
———
Termination proved for g’, but not proved for g and g’’ !!
module Test
use import int.Int
use import int.EuclideanDivision
let p x = mod x 2 = 0
(* *)
let rec f e =
requires
Dear Jens + Yannick,
I have similar problems with ‘why3’ and ‘cvc4 1.5’ weaker than ‘cvc4 1.4’
-JJ-
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Hello Friends!
> Le 18 oct. 2017 à 13:15, Jean-Jacques Levy <jean-jacques.l...@inria.fr> a
> écrit :
>
> Hello everybody!
>
> I installed why3 0.88.0 and coq 8.6.1 with opam. I get following error
> message:
>
> Compiled library Why3.BuiltIn (in file
> /
used ?
Best to all, -JJ-
> Le 25 mars 2019 à 17:55, Andrei Paskevich a écrit :
>
> Dear Jean-Jacques,
>
> "val constant nn : int" should do the trick.
>
> Best,
> Andrei
>
> On Mon, 25 Mar 2019 at 17:54, Jean-Jacques Levy <mailto:jean-jacques
Dear Friends,
in Why3.1.2.0, it looks that functions got an implicit ‘ghost' tag :
module DDD
use int.Int
use list.List
use map.Map
type vertex = int
function infty (): int = 1000
let function myset (f: map vertex int) (x: vertex) (v: int) : map vertex
I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-
> Le 21 févr. 2019 à 16:46, Julia Lawall a écrit :
>
>
>
> On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:
>
>>
>> Hello,
>>
>> Use the keyword `by`:
>>
>> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by
variant { s }
>>> ...
>>>
>>> The definition is now accepted.
>>>
>>> You may wonder why function ([<-]) was declared ghost in the first
>>> place. This is because polymorphic equality is hidden behind this
>>> function. Fun
the functor Set.Make in OCaml.
>
> Longer answer, of the previous mail too, should come soon...
>
> - Claude
>
> Le 19/02/2019 à 15:33, Jean-Jacques Levy a écrit :
>> Dear Jean-Christophe + Friends,
>> me again (* sorry *) .. a quick view about polymorphic equ
Dear Friends,
in why3.1.2.0, I cannot succeed in passing an argument to command in line 0/0/0
!!
-
goal list_simpl_r :
forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
-
Following hypothesis was not found: l1
ok.. merci. Mais en mettant l’attribut [@induction] (nouvelle syntaxe), je dois
faire induction_ty_lex et destruct l2 !!
Why3.1.2.0 serait-il un (autre) nouveau nom pour Coq ?
A+, -JJ-
> Le 22 févr. 2019 à 14:56, Sylvain Dailler a écrit :
>
> On 22/02/2019 13:50, Jean-Jacques L
ossible ghost fields that
> would be erased at runtime), we have no other choice than forbidding its
> use in regular (i.e. non-ghost) code.
>
> As for your question "where to insert the ghost keyword", you can find
> the answer on page 87 in the PDF manual, Fig.
Dear Why3 Friends,
is there any doc about the functionality of the "Inline" button in the Why3
IDE ?
Same for inline_all, inline_goal, inline_trivial..
My current problem is that the inlined version of a trivial function works with
automatic provers, but I cannot find a way of forcing that
ot;unfold foo" where
> "foo" is your function symbol. The documentation is also visible
> interactively.
>
> I don't know how to help more without seeing the exact example you have.
>
> - Claude
>
>
>
> Le 14/02/2019 à 16:20, Jean-Jacques
Dear Jean-Christophe + Friends,
me again (* sorry *) .. a quick view about polymorphic equality:
Equality in logic should be distinct from Equality in regular code, where the
ghost attribute is prohibited. So if the problem with the ghost values is only
about aggregated data with ghost
Dear Andrei,
I’m also slow because of travelling to Nice...
> Le 28 mai 2019 à 15:27, Andrei Paskevich a écrit :
>
> Dear Jean-Jacques,
>
> very late and very partial answer:
>
> On Wed, 10 Apr 2019 at 17:38, Jean-Jacques Levy <mailto:jean-jacques.l...@inria.fr>
Guillaume,
« trigger » ?? meaning? Is it in Why3 manual? I guess it’s related to
attributes such as [@induction], but not sure..
Thanks for info, -JJ-
> Le 10 mai 2019 à 08:30, Guillaume Melquiond a
> écrit :
>
> Le 10/05/2019 à 00:19, Евгений Макаров a écrit :
>
>> Both lemmas are proved
Dear Guillaume (and Andrei),
> Le 16 mai 2019 à 17:04, Guillaume Melquiond a
> écrit :
>
> Le 16/05/2019 à 16:58, Jean-Jacques Levy a écrit :
>
>> can you insert the attribute when the ‘if-statement’ is not in the logic but
>> is in the code ?
>> let f (b
35 matches
Mail list logo
