why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-07-17T15:44:03+02:00https://gitlab.inria.fr/why3/why3/-/issues/716micro-Python: add slice assignment2023-07-17T15:44:03+02:00Jean-Christophe Filliâtremicro-Python: add slice assignmentAdd support for slice assignment, that is,
```
e1[e2:e3] = e4
```Add support for slice assignment, that is,
```
e1[e2:e3] = e4
```Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/681Support unicode strings2022-11-16T13:33:44+01:00Xavier DenisSupport unicode stringsIt seems like the grammar of strings in Why3 is limited to ascii strings, but the corresponding SMT theory specifically supports unicode strings.
We don't even need to support parsing utf-8 strings so long as we allow longer escape seq...It seems like the grammar of strings in Why3 is limited to ascii strings, but the corresponding SMT theory specifically supports unicode strings.
We don't even need to support parsing utf-8 strings so long as we allow longer escape sequences for individual characters up to `0x2FFFF`. However, since currently `char` is mapped to OCaml's `char` type this introduces a conflict.https://gitlab.inria.fr/why3/why3/-/issues/642Use Python's type variables2022-04-28T08:54:54+02:00Guillaume MelquiondUse Python's type variablesWhy3's Python plugin uses the syntax `'foo` to denote type variables. But Python actually provides type variables, so it might be better to use them, rather than use our own incompatible syntax:
```python
from typing import TypeVar
T = T...Why3's Python plugin uses the syntax `'foo` to denote type variables. But Python actually provides type variables, so it might be better to use them, rather than use our own incompatible syntax:
```python
from typing import TypeVar
T = TypeVar('t')
def repeat(x: T, n: int) -> list[T]:
return [x]*n
```
The parser would have to explicitly recognize the statement `ident = TypeVar(expr)` and register `ident` as denoting a type variable. Another possibility would be to just disregard the statement and assume that any identifier not recognized as a type is a type variable.Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/552RFC: binders for tuple components in function prototype2021-02-11T10:43:19+01:00Jean-Christophe FilliâtreRFC: binders for tuple components in function prototypeIt would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it ...It would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it in every clause of the contract:
```
val f (p: (int, int)) : (r: int)
requires { let x, y = p in x < 0 && y > 0 }
ensures { let x, y = p in r = x + y }
```https://gitlab.inria.fr/why3/why3/-/issues/547Syntactic sugar for lemma functions2021-04-09T08:27:17+02:00Loïc CorrensonSyntactic sugar for lemma functionsThe following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs...The following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs } ensures { p } [variant {v}] = begin t end
[with …]
```https://gitlab.inria.fr/why3/why3/-/issues/531Add a deriving framework for WhyML2021-02-11T10:36:18+01:00François BobotAdd a deriving framework for WhyMLFollow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?Follow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?https://gitlab.inria.fr/why3/why3/-/issues/519When clauses2021-01-29T07:27:18+01:00Xavier DenisWhen clausesI promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from langu...I promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from languages with support for this functionality.
The challenge with adding this functionality to why3 is that patterns are desugared quite late in the compilation pipeline. Since we would like to desugar a constant pattern into an equality test, this is problematic as we must correctly resolve `=` for the type of the matched constant.
An alternative approach which is also more general would be to introduce `when` clauses. In this approach, match arms could be annotated with any boolean valued function. This function would have access to any binders created by the match arm's patterns. As this function would get typechecked with the rest of the AST, by the time we get to case-desugaring we should have no difficulty transforming it into a boolean test.
---
During a GT a few weeks ago we discussed this and several challenges and alternative solutions were proposed, unfortunately I didn't take notes at time and I no longer recall them.https://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T13:19:54+01:00DAILLER 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 t...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/389Add "final" specifier2021-02-11T10:39:53+01:00Raphaël Rieu-HelftAdd "final" specifierIt could be used for private types that we do not want to be refinable.It could be used for private types that we do not want to be refinable.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/278Parsing on attributes in programs2022-06-24T11:44:12+02:00DAILLER SylvainParsing on attributes in programsHello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be neede...Hello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/246Allow "use ghost Foo"2019-05-21T15:37:41+02:00Guillaume MelquiondAllow "use ghost Foo"It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted prog...It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?https://gitlab.inria.fr/why3/why3/-/issues/27Sequence literals2020-12-17T10:27:16+01:00Guillaume MelquiondSequence literalsCurrently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data struct...Currently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
1. What is the syntax? The OCaml syntax `[| ... ; ... |]` might be fine.
2. What is the type of such a literal? Should it have a fixed type (e.g. `seq 'a`)? Or should its type depend on the context so that one can use this syntax to input program arrays?
3. How should it be translated to provers that do not support such literals? Using `epsilon s. length s = ... /\ s[0] = ... /\ ...` might be both effective and cheap implementation-wise.