README.md

Stainless

Hosted at https://github.com/epfl-lara/stainless ; mirrored at https://gitlab.epfl.ch/lara/stainless

Verification framework for a subset of the Scala programming language. See the tutorial.

Please note that this repository uses git submodules, so you need to either:

• clone it with the --recursive option, or
• run $ git submodule update --init --recursive after cloning.

Please note that Stainless does not support Scala 2 frontend anymore but only Scala 3.3. The latest release that does support Scala 2.13 frontend is the v0.9.8.7.

Quick start

We test mostly on Ubuntu; on Windows, you can get sufficient text-based Ubuntu environment by installing Windows Subsystem for Linux (e.g. wsl --install, then wsl --install -d ubuntu). Ensure you have a Java version ready (it can be headless); on Ubuntu sudo apt install openjdk-17-jdk-headless suffices.

Once ready, Download the latest stainless-dotty-standalone release for your platform. Unzip the archive, and run Stainless through the stainless script. Stainless expects a list of space-separated Scala files to verify but also has other Command-line Options.

To check if everything works, you may create a file named HelloStainless.scala next to the stainless script with the following content:

import stainless.collection._
object HelloStainless {
  def myTail(xs: List[BigInt]): BigInt = {
    require(xs.nonEmpty)
    xs match {
      case Cons(h, _) => h
      // Match provably exhaustive
    }
  }
}

and run stainless HelloStainless.scala. If all goes well, Stainless should report something along the lines:

[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                    ║
[  Info  ] ║ HelloStainless.scala:6:5:   myTail  body assertion: match exhaustiveness  nativez3   0,0 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 1    valid: 1    (0 from cache) invalid: 0    unknown: 0    time:     0,0         ║
[  Info  ] ╚══════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Shutting down executor service.

If you see funny symbols instead of the beautiful ASCII art, run Stainless with --no-colors option for clean ASCII output with standardized error message format.

The release archive of Stainless only requires JDK17. In particular, it needs neither a Scala compiler nor SBT. It is shipped with Z3 4.12.2, cvc5 1.0.8 and Princess. If Z3 API is not found, use option --solvers=smt-z3 to rely on the executable.

SBT Stainless plugin

Alternatively, one may integrate Stainless with SBT. The supported Scala versions is 3.3.3. To do so, download sbt-stainless, and move it to the directory of the project. Assuming the project's structure is:

MyProject
├── build.sbt
├── project
│   └── build.properties
├── sbt-stainless.zip
└── src/

Unzipping sbt-stainless.zip should yield the following:

MyProject
├── build.sbt
├── project
│   ├── build.properties
│   └── lib                     <--------
│       └── sbt-stainless.jar   <--------
├── sbt-stainless.zip
├── src/
└── stainless/                  <--------