On Sun, 6 Dec 2020, Laurent Thery wrote:
> >
> > Is there any hope for getting a better solution? I upgraded my server,
> > and seem to have lost whatever I had done.
> >
>
> Note that you can put your change locally in
>
> ~/.local/share/gtksourceview-3.0/styles/
Thanks for the suggestion.
Hello,
Our discussion about colors in why3 over the summer ended with the
following suggestion from Andrei:
---
As a quick and ugly measure I would probably just hack
/usr/share/gtksourceview-3.0/styles/classic.xml, which seems to be the
default.
---
Is there any hope for getting a better
Previously there was a discussion about what terms should be colored for
the case of a VC that is associated with re-establishing a type invariant
at the end of a function.
It seems that if the function ends with a sequence of ifs, then for a tpye
invariant the whole if is colored. On the other
On Tue, 16 Jun 2020, Andrei Paskevich wrote:
> Hi Julia,
>
> if I understand correctly the problem, you may want to look at the file
> share/lang/why3.lang — it contains the description of WhyML grammar, and the
>
idered to be in some
categories, perhaps I could figure out how to globally change the colors
associated with these categories.
thanks,
julia
>
> On Fri, Jun 12, 2020 at 6:15 PM Julia Lawall wrote:
>
>
> On Fri, 12 Jun 2020, Benoit Rognier wrote:
>
> > Hi Ju
e
> print_time_limit = true
> saving_policy = 1
> show_full_context = false
> task_height = 633
> tree_width = 519
> verbose = 0
> window_height = 896
> window_width = 1339
Thanks! I was just looking at what can be configured in the GUI, but I
see that there are more optio
On Fri, 12 Jun 2020, Benoit Rognier wrote:
> Hello
> yes because it uses gtk(2?) technology. so you need to install a dark gtk
> theme.
> which os are you using? if not Linux, it can be a bit bumpy to configure.
> I did so on macos last year and it took some external libs to install the
> gtk
stall the
> gtk theme switcher (via brew I guess)
Hmm, I'm running why3 on a remote server. It has some form of Ubuntu.
I'll see how I can change its theme.
thanks,
julia
>
> regards,
> Benoit
>
>
>
> On Fri, Jun 12, 2020 at 1:43 PM Julia Lawall wrote:
&g
Is there a dark theme for the IDE?
thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Recently I was told that there was a regression in the code for matching
proofs to VCs on reloading a file. I did a pull and things seemed to work
much better. But now I have the impression that things are not working so
well again. For example, I have a goal that is just true, and it is
Hello,
I receiced the following message. It says to report it, so I am reporting
it. But I wouldn't know how to reproduce it.
exception 'anomaly:
Why3.Controller_itp.Make(S).TransAlreadyExists("split_vc", "")' was raised
in a LablGtk callback.
This should not happen. Please report.
julia
On Sat, 28 Mar 2020, Guillaume Melquiond wrote:
> Le 28/03/2020 à 11:16, Julia Lawall a écrit :
> > Does saving preferences impact the .why3.config file? I change the editor
> > for cvc4 and click on save, but when I leave why3 and restart it,
> > the value that I saved i
On Thu, 26 Mar 2020, Guillaume Melquiond wrote:
> Le 26/03/2020 à 13:08, Julia Lawall a écrit :
>
> > Are there any other possibilities, or other ways to solve the problem of
> > finding useless asserts?
>
> I don't have any good solution. But here are a few ideas tha
Hello,
I suspect that my proofs have too many asserts. However, I'm not
courageous enough to comment them out by hand one by one to find the ones
that are not necessary.
I tried making a tool to generate a copy of the file with each assert
removed, and to copy the session and update the name of
Hello,
I am using 54b1573501a388c3d9d22c225b7c0857a139bc12.
It seems that in the ide, the line numbers on error messages hve
disappeared? I still see the line number with why3 prove.
thanks,
julia
___
Why3-club mailing list
It's not clear to me how why3 session update works. I have a file called
system.mlw, and thus a session directory called system. I tried why3
session update -rename-file system xxx and I obtain no file containing xxx
in its name and grep -r xxx turns up nothing. I did why3 session update
On Wed, 25 Mar 2020, Claude Marche wrote:
>
>
> 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 t
I see the option --apply-transform to apply a specific transform, but is
it possible to apply a strategy, as defined in the .why3.conf file?
thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
On Sun, 22 Mar 2020, Andrei Paskevich wrote:
> Hi Julia,
>
> when you call a let-lemma in your code, it behaves in exactly the same way
> as a normal function call: you must supply the parameters and prove the
> instantiated preconditions. These preconditions do not stay in the context
> for the
Hello,
I have the impression that when using a let lemma as code, one gets asked
to prove all the preconditions, that then clutter up the space of known
things, making other things harder to prove. In my case, I have to add a
lot of let x = pure { y } declarations to be able to use the let
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>
> >> As far as I know, the strategies have not changed since they were
> >> renamed, so I have no idea why you are experiencing a change of behavior
> >>
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 22:14, Julia Lawall a écrit :
>
> >> As far as I know, the strategies have not changed since they were
> >> renamed, so I have no idea why you are experiencing a change of behavior
> >>
> * default proof strategies "Auto level 1" and "Auto level 2"
> have been respectively renamed "Auto level 2" and "Auto level 3";
> "Auto level 1" now behaves similarly to "Auto level 0" but with a longer
> time limit; more details in the manual, Section 10.6 "Proof Strategies"
>
There remains the problem that Auto Level 3 goes into an infinite loop,
at least when the goal is a predicate.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
On Wed, 18 Mar 2020, Claude Marche wrote:
>
>
> Le 18/03/2020 à 14:39, Julia Lawall a écrit :
> > The problem seems ot be the --strings-exp option. If I remove that, cvc4
> > seems to work fine.
>
> Thanks for the feedback. We will do our best to fix this pr
The problem seems ot be the --strings-exp option. If I remove that, cvc4
seems to work fine.
julia
diff --git a/share/provers-detection-data.conf
b/share/provers-detection-data.conf
index a85e609e4..eac39d396 100644
--- a/share/provers-detection-data.conf
+++
On Wed, 18 Mar 2020, Claude Marche wrote:
>
> 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
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 12:28, Julia Lawall a écrit :
>
> > What should I do to get why3 to use the right file? I tried rerunning
> > make, but it didn't do anything. Do I need to change my configuration
> > file somehow?
>
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 10:48, Julia Lawall a écrit :
> > When I run cvc4 on the command line, it ends with
> >
> > (error "Can't get-info :reason-unknown when the last result wasn't
> > unknown!")
> >
> &g
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 09:21, Julia Lawall a écrit :
>
> > I have the impression that it is using drivers/cvc4-realize.drv. I made
> > the change you suggested, but if I edit the cvc4 proof, it shows
> > ALL_SUPPORTED. Or is
On Wed, 18 Mar 2020, Guillaume Melquiond wrote:
> Le 18/03/2020 à 08:45, Julia Lawall a écrit :
> > Could the generated code be bigger than before? I tried cvc4 on a proof
> > that is simple and has few dependencies and it was fine.
>
> Among the things that changed re
J'ai aussi l'impression d'avoir une boucle infinie sur un auto level 3.
Il fait des split_vc infiniement, mais a chaque etape le but est un
predicate, et il n'y a rien a splitter.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
cvc4 1.7 a l'air de me donner systematiquement un seg fault:
CVC4 suffered a segfault.
Offending address is 0x7fff8
expr::ExprManager::AND, 736
expr::ExprManager::APPLY_UF, 4555
expr::ExprManager::BOUND_VARIABLE:Boolean type, 11
expr::ExprManager::BOUND_VARIABLE:integer type, 663
Hello,
I wonder if there is some easy room for improvement in the process of
reloading a session when things have changed. For example, I have at
least the illusion that when I remove a lemma at the end of a large module
and then reload it, the proofs don't all end up in the right places.
For
On Mon, 14 Oct 2019, Sylvain Dailler wrote:
> Le 14/10/2019 à 14:31, Guillaume Melquiond a écrit :
> > Le 14/10/2019 à 07:59, Julia Lawall a écrit :
> >> My configuration file contains:
> >>
> >> error_color = "red"
> >> er
x } in ..." You may then call your let lemma on
> ox at a later point.
OK, thanks.
julia
>
> Raphaël
>
> On 03/10/2019 11:30, Julia Lawall wrote:
> > It seems that I cannot use (old ...) in calling my let lemma? Is there a
> > way around this?
> >
> &g
It seems that I cannot use (old ...) in calling my let lemma? Is there a
way around this?
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
On Thu, 3 Oct 2019, Claude Marche wrote:
>
>
> 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 -> cor
On Thu, 3 Oct 2019, Claude Marche wrote:
>
>
> 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
> >
On Thu, 3 Oct 2019, Claude Marche wrote:
>
>
> 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 t
> location where the lemma should be used
I don't follow this at all. My lemma is in a different file than the
place where I want to use it. So I guess that the name space is polluted
anyway?
julia
>
> - Claude
>
> Le 02/10/2019 à 10:00, Guillaume Melquiond a écrit :
> > Le 01/1
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.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
On Wed, 2 Oct 2019, Guillaume Melquiond wrote:
> Le 01/10/2019 à 17:52, Julia Lawall a écrit :
> > Hello,
> >
> > I have to resort to some explicit applys. When I then change my .mlw
> > file, it seems that the why3 proof realignment rarely puts the existing
&g
Hello,
I have to resort to some explicit applys. When I then change my .mlw
file, it seems that the why3 proof realignment rarely puts the existing
applys in the right place. At some times I have thought that they are
backwards, but I have't studied that in detail.
Is there any way to put the
On Tue, 3 Sep 2019, Claude Marche wrote:
>
> Hello,
>
> For the record, if others have the same issue:
>
> rm lib/why3/why3extract.cmi
>
> should solve the problem
Works. Thanks!
julia
>
> - Claude
>
> Le 03/09/2019 à 08:07, Guillaume Melquiond a écri
> On 3 Sep 2019, at 08:07, Guillaume Melquiond
> wrote:
>
>> Le 03/09/2019 à 07:54, Julia Lawall a écrit :
>> With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the
>> following:
>> File "src/tools/why3extract.ml", line 1:
>> E
With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the
following:
File "src/tools/why3extract.ml", line 1:
Error: The implementation src/tools/why3extract.ml
does not match the interface lib/why3/why3extract.cmi:
The module `Why3__Matrix' is required but not provided
[@inline:trivial] on the definition of a predicate is useful because it
allows proofs to directly use the definition of the predicate. But it
seems to also make it hard to prove that a use of a predicate follows from
itself. Eg if pred has this annotation, then having
pred a b c d
as a
_from_current with (old p.cores),p.cores,core,i,dst,t,c
Transformation failed.
On argument:
(old p.cores),p.cores,core,i,dst,t,c
Parsing error: `at' and `old' can only be used in program annotations
julia
>
> Hope this helps,
> --
> Jean-Christophe
>
> On 7/13/19 9:12 AM, Julia Lawal
;
> you can do
>
> apply L with 21,21
>
> Then the value for "y" (42) is inferred when matching the goal and the
> lemma's conclusion, and you are thus providing values for "x" and "z",
> in that order.
>
> Hope this helps,
Thanks!
I guess the apply transformation is a way to force a lemma to be used at a
particular place in a proof? How does one specify the list of arguments,
ie a value of list term type?
thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
I obtained the following with the master from the why3 gitlab:
warning: [Session_itp.merge_trans] FATAL unexpected exception: anomaly:
Not_found
This came after commenting some code in the IDE, and then I think save and
refresh. After restarting why3, all is fine, so I don't especially care
Is there an easy way to take a single mlw file and be sure that all of the
modules that it relies on have been fully proved?
Is there an easy way to obtain a list of all of the modules that a given
file or module relies on?
thanks,
julia
___
Why3-club
Indeed, regardless of the multiplier, I never see more than around 20
alt-ergo processes running, even though I asked for 40. So I guess that
most of the time is used on generating the verification conditions.
julia
___
Why3-club mailing list
On Sat, 20 Apr 2019, Andrei Paskevich wrote:
> Sorry, I meant each 0.1 sec, of course.
>
> The 3x factor is, if I remember correctly, the upper bound on the backlog
> size: Why3 stops preparing tasks once it has 3x#cores tasks ready to go. I
> don't think lowering it is a good solution
On Sat, 20 Apr 2019, Andrei Paskevich wrote:
> Indeed, with as many as 47 cores ready to run external provers, Why3 is sure
> busy to fill the working queue with prepared proof tasks. I am not sure what
> is the right approach here: set some real-time bounds and go back to UI,
> say, each tenth
On Sat, 20 Apr 2019, Guillaume Melquiond wrote:
> Le 19/04/2019 à 13:41, Julia Lawall a écrit :
>
> >> 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
> >> hav
rocesses
> of your system.
I asked for 47.
But even if there are only eg 10 things to prove, I still see a
smaller but noticible delay.
But if there is nothing obvious, I will try to look into it later.
thanks,
julia
>
> - Claude
>
> Le 18/04/2019 à 11:35, Julia Lawall a éc
ee to provide such a module A__X by any means.
That sounds fine. Thanks!
julia
>
> Hope this helps,
> --
> Jean-Christophe
>
> >> Le 14/04/19 à 18:51, Julia Lawall a écrit :
> >>
> >>
> >> On Sun, 14 Apr 2019, Mario Pereira wrote:
> >>
> &g
tion
[val random_int: unit -> {} int {}]
is typically enough.
I could try Random, which seems simple enough. But I also need a random
value of one of my own types.
Couldn't the extraction just leave undefined things as undefined?
julia
>
> Best regards
> --
> Mário
>
>
was
getting previously.
julia
>
> Thank you in advance.
>
> Best regards
> --
> Mário
>
> Le 12/04/19 à 22:34, Julia Lawall a écrit :
>
>
> On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote:
>
> I think I managed t
On Fri, 12 Apr 2019, Mario Pereira wrote:
> > Do you have any suggestions of what to look for?
>
> It would maybe be helpful for me to debug the problem to know if this comes
> from pattern or type extraction.
>
> When you are calling the extraction engine, could you please add to your
>
why3 extract is tripping on the assert in the following code (MaskGhost
case):
(* remove ghost components from tuple, using mask *)
(* TODO : completely remove this function *)
let visible_of_mask m sl = match m with
| MaskGhost-> assert false (* FIXME ? *)
| MaskVisible -> sl
On Sun, 7 Apr 2019, Mario Pereira wrote:
> Hello,
>
> I believe you can resort to *ghost results* in order to solve this
> issue. In Why3, a function can return multiple results, some of them
> marked as ghost.
>
> For instance:
>
> let f (x: int) : (r: int, ghost rg: int)
> ensures { r
it to the issue tracker as a suggestion.
julia
>
> Best regards,
> --
> Jean-Christophe
>
> On 4/6/19 8:38 AM, Julia Lawall wrote:
> > Hello,
> >
> > I tried to make the following strategy:
> >
> > [strategy]
> > code = "start:
> > t inline_g
On Sat, 6 Apr 2019, Andrei Paskevich wrote:
> Hi Julia,
>
> On Sat, 6 Apr 2019 at 17:03, Julia Lawall wrote:
> > I am somewhat lost at different types of functions in Why3. I
> > understand that there are pure logical functions and program
> > f
On Sat, 6 Apr 2019, Евгений Макаров wrote:
> Hello,
>
> I am somewhat lost at different types of functions in Why3. I
> understand that there are pure logical functions and program
> functions, but I am confused by different types of declarations. Here
> are my questions.
>
> What is the
Hello,
I tried to make the following strategy:
[strategy]
code = "start:
t inline_goal afterinline
afterinline:
t split_vc aftersplit
aftersplit:
c Alt-Ergo,2.3.0 %t %f
"
desc = "Inline@ then@ split"
name = "InlineSplit"
It gives a parse error on the c at the beginning of the last line. What
On Thu, 4 Apr 2019, Sylvain Dailler wrote:
> On 03/04/2019 20:35, Julia Lawall wrote:
> > > >The smoke detector is parallel
> > > > to the splint in each case, and times out in each case. When I replay
> > > > this file with the smoke detector option
The why3 manual says that the smoke detector can give false positives in
the case of unreachable code. Is there any way to avoid this? I have an
unreachable match case. I tried putting absurd in the code, but I still
get a smoke detected report.
thanks,
julia
On Wed, 3 Apr 2019, Sylvain Dailler wrote:
> Sorry for the delay.
>
> On 03/04/2019 11:53, Julia Lawall wrote:
> > OK, sorry, I don't know. I tried it again just now, and it sent alt-ergo
> > to both subgoals, the children of the split and the children of thesmoke
>
On Wed, 3 Apr 2019, Sylvain Dailler wrote:
> On 03/04/2019 10:31, François Bobot wrote:
> > So perhaps you both agree that we should hide the smoke detector
> > transformation but we should not
> > hide the smoke detector functionnality in the IDE.
>
> Ideally, I would tend to agree with this,
On Wed, 3 Apr 2019, François Bobot wrote:
> Le 03/04/2019 à 10:22, Julia Lawall a écrit :
> > On Wed, 3 Apr 2019, Sylvain Dailler wrote:
> >>
> >> Perhaps, we should hide this kind of transformations from the IDE ?
> >>> Is
> >>> there a way
On Wed, 3 Apr 2019, François Bobot wrote:
> Le 02/04/2019 à 14:15, Julia Lawall a écrit :
> > Having discovered the commandline, I also found the command smoke
> > detector. Running that command makes a lot of proof obligations. Is
> > there a way to click once and get
Having discovered the commandline, I also found the command smoke
detector. Running that command makes a lot of proof obligations. Is
there a way to click once and get them all to be proved at once?
thanks,
julia
___
Why3-club mailing list
On Fri, 29 Mar 2019, Claude Marche wrote:
>
>
> 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
On Fri, 29 Mar 2019, Claude Marche wrote:
>
> 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 use this a lot as
gt; majority
> of the automated provers via their drivers. Alternatively, you can call apply
> "inline_trivial" in the IDE to force the inlining during the interactive
> phase.
Great! Thanks so much for taking care of it quickly.
julia
>
> Best,
> Andrei
>
> On
h inline. I know
up front that they only exist to collect information and reduce code size.
The split_goal limitation is not a problem.
Could this be done quickly, or would it have to wait for the next release?
Thanks,
julia
>
> Best,
> Andrei
>
> On Mon, 25 Mar 2019 at 08:57,
My natural inclination is to make predicates that combine other
predicates, in order to avoid massive code duplication. But it seems that
doing so makes it very hard for why3 to find the information it needs. So
to get the proof to go through, I have to manually inline the predicates,
which
Thanks!
julia
>
> Best regards
> --
> Mário
>
> Le 20/03/19 à 10:49, Julia Lawall a écrit :
> >
> > On Wed, 20 Mar 2019, Jean-Christophe Filliatre wrote:
> >
> >> Dear Julia,
> >>
> >> With a goal as simple as
> >>
> >&
e problem. I was hoping that constants
would be just inlined away, like for a #define in C. But perhaps there
are good reasons for not doing that.
thanks,
julia
>
> Best regards,
> --
> Jean-Christophe
>
> On 3/19/19 10:36 PM, Julia Lawall wrote:
> > I have some definitions
I have some definitions:
let constant realtime = 0
let constant timeshare = 1
However, subsequently why3 seems to have trouble proving things involving
these values, particularly things that involve knowing that realtime and
timeshare don't have the same value. Inlining the values makes the
c, p, t or a label.
Thanks for the explanation and the pointer to the relevant section of the
manual.
julia
>
> - Claude
>
> Le 16/03/2019 à 09:17, Julia Lawall a écrit :
> > Often I do split_vc and the alt-ergo. How would I define such a strategy
> > in the configuration
Often I do split_vc and the alt-ergo. How would I define such a strategy
in the configuration file?
I tried:
[strategy]
code = "start:
t split_all_full
c Alt-Ergo,2.0 40 1
But it says "Fatal: loading strategy 'Auto_level_1' failed: syntax error
on character 'A' at position 26"
I see
got this to work. Actually my lemma is declared with let rec
lemma. Why3 says that it is not a proposition.
julia
>
> Hope this helps,
>
> Le 04/01/2019 à 16:48, Julia Lawall a écrit :
> > Is it possible to make a lemma only visible within a module, but not
> > v
ot; predicate foo
>
> Unless I'm mistaken, there is no way to indicate the opposite i.e. that
> a symbol must always be inlined.
OK, I've been sprinkling
meta "rewrite_def" proposition foo
But I'm not sure if it really has an impact...
julia
>
> Best regards,
> --
&
Hello,
Is there an annotation that can be put in a .mlw to cause a predicate
always to be inlined? Currently, I have to guess when inline_goal or
inline_all would be useful, and neither is really satisfactory, because I
don't want to inline everything, but just this one predicate.
thanks,
julia
On Thu, 21 Feb 2019, Jean-Jacques Levy wrote:
> I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-
I'll look into that, thanks.
julia
>
> > Le 21 févr. 2019 à 16:46, Julia Lawall a écrit :
> >
> >
> >
> > On Thu, 21 Feb 2019, Raphael R
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 { x =
> Array.make 1 1 }
Is by useful for anything else? Sometimes I know that a particular lemma
should be useful for proving
On Mon, 18 Feb 2019, Jean-Jacques Levy wrote:
> Dear Jean-Christophe and Friends,
> thanks for your answer. So you avoid inconsistent use of equality for records
> with ghost fields by preventing its usage in regular code. (I have still to
> understand the meaning of the ‘pure’ attribute).
On Wed, 30 Jan 2019, François Bobot wrote:
> Le 30/01/2019 à 13:36, Julia Lawall a écrit :
> > I have the following orgnization of modules:
> >
> > A parameterized by f
> >
> > B uses A
> >
> > C uses A and B and is parameterized by g
> >
&g
Hello,
I have the following orgnization of modules:
A parameterized by f
B uses A
C uses A and B and is parameterized by g
D uses A, B and C and provides a definition for f and for g
The definition for g relies on things defined in A and B.
How can I set this up? In D, I cannot just clone
In the following:
val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = (old a)[i <- v] }
a = (old a)[i <- v] implies a.elts = Map.set (old a).elts i v
why3.1.1.1/src/driver/call_provers.ml: | OutOfMemory -> fprintf fmt "Ouf Of
Memory"
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
> On 24/01/2019 14:37, Julia Lawall wrote:
> > Are there some particular arguments that why3 provides to alt-ergo? Now I
> > am just running a proof in altgr-ergo, and it has been running for more
> > than 5 minutes with no r
Are there some particular arguments that why3 provides to alt-ergo? Now I
am just running a proof in altgr-ergo, and it has been running for more
than 5 minutes with no result - it looks like an infinite loop. But from
within why3, the lemma is accepted in around 30 seconds.
julia
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
>
> On 24/01/2019 13:50, Julia Lawall wrote:
> >
> > On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
> >
> > > Hello,
> > >
> > > You can use "alt-ergo -profiling N " to display
s
> that do not appear in the .used file corresponding to the input
> file.
Does this work from why3? I tried adding the -verbose option in the why3
configuration file, and I have the impression that why3 wrote over it. I
don't know whay information why3 feeds to alt-ergo, so I don't know how to
ru
On Tue, 8 Jan 2019, Claude Marché wrote:
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
Is there any way to find out what lemmas alt-ergo is trying to use? This
could be helpful to figure out what to
1 - 100 of 130 matches
Mail list logo
