why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-11-27T12:19:54Zhttps://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T12:19:54ZDAILLER Sylvaintype invariant preservation questionI have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```https://gitlab.inria.fr/why3/why3/-/issues/315Too much ghostification?2021-03-12T23:30:35ZBenedikt BeckerToo much ghostification?In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from line 16, or when an `; ()` is added after line 16.
```
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
```In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from line 16, or when an `; ()` is added after line 16.
```
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
```1.5.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/287Add injectivity for type invariant2021-02-05T14:04:11ZFrançois BobotAdd injectivity for type invariant```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
```
# Decision #
> So, we agreed that adding `t'mk` for constructing a non-private type `t` from its fields is a good idea.```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
```
# Decision #
> So, we agreed that adding `t'mk` for constructing a non-private type `t` from its fields is a good idea.1.5.0François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/171Extraction of absurd2020-10-23T15:36:51ZMARCHE ClaudeExtraction of absurdExtraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
```
# <line number> <mlw file name>
```
on the line before ```assert false```Extraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
```
# <line number> <mlw file name>
```
on the line before ```assert false```PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/30Refresh does not reload source view, causing loss of work2019-10-25T13:12:27ZRaphaël Rieu-HelftRefresh does not reload source view, causing loss of workRefreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)Refreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)MARCHE ClaudeMARCHE Claude