stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
In situations like this: ```scala case class Nat(n: BigInt){ require(n > 0) } def foo(n: Nat): Unit = { { n ==:| aProof |: Nat(complicatedFunction) }.qed // or: assert( n...
Stainless version: ``` [ Info ] Stainless verification tool (https://github.com/epfl-lara/stainless) [ Info ] Version: 0.9.1 [ Info ] Built at: 2021-09-28 12:09:18.155 [ Info ] Bundled Scala compiler version: 2.13.6...
We had an example where we need to assume a recursive function to be opaque while we verify it, but later we want to see its body to prove an...
When I save a file that Stainless tracks in watch mode, Stainless outputs `Detected file modifications` while the file contents actually didn't change.
Can we report counterexamples as valid Scala test functions that (at least in some cases) apply to the initial source code (before the transformations). The user can then paste these...
```scala import stainless.lang._ import stainless.annotation._ object GhostMatch { case class Foo(@ghost value: Option[BigInt]) def nonGhostMatch(foo: Foo) = { foo match { // should fail because foo.value will not exist at...
We could inject certain free assumptions in verification that correspond to the existence of a stripped down function that is generated during ghost erasure. Given: ```scala def f(x: Int, @ghost...
The following example *sometimes* leads to `TypeChecker` complaining about an illegal recursive call: ```scala import stainless.lang._ import stainless.annotation._ import stainless.collection._ import stainless.proof._ object NodeCycleExample { case class Node(var next: Option[Node])...
Discussion on May 7th 2021 **Jad**: Is there a workaround to avoid type-encoding for something like that? https://gist.github.com/jad-hamza/d5b4ce6b3d8e0fec7ca18e786c7ac4bf I tried to use the SortedArray in another file, but this requires...
We currently stored non-normalized types in pattern matches. For instance, we might have a case with an ADT pattern ```scala def size[T](xs: List[T]): BigInt = xs match { case Nil...