# Introduction¶

The Stainless verification framework aims to help developers build verified Scala software. It encourages using a small set of core Scala features, but provides unique automation functionality. In particular, Stainless can

- verify statically that your program conforms to a given specification and that it cannot crash at run-time
- provide useful counterexamples when an implementation does not satisfy its specification
- verify that your program will terminate on all inputs

## Stainless and Scala¶

Stainless attempts to strike a delicate balance between the
convenience of use on the one hand and the simplicity of
reasoning on the other hand. Stainless supports verification
of Scala programs by applying a succession of semantic-preserving
transformations to the Pure Scala fragment until
it fits into the fragment supported by
Inox.
The Pure Scala fragment is at the core of
the functional programming paradigm and lies at the intersection
of functional languages such as Scala, Haskell, ML, and fragments
present in interactive theorem provers such as Isabelle and Coq. Thus,
if you do not already know Scala, learning the Stainless subset should
be easier as it is a smaller language. Moreover, thanks to the use of
`scalac`

front end, Stainless supports implicits and `for`

comprehensions (which also serve as a syntax for monads in Scala).
Stainless also comes with a simple library of useful data types, which
are designed to work well with automated reasoning and Stainless’s
language fragment.

In addition to this pure fragment, Stainless supports certain imperative features. Features thus introduced are handled by a translation into Pure Scala concepts. They are often more than just syntactic sugar, because some of them require significant modification of the original program, such as introducing additional parameters to a set of functions. As an intended aspect of its current design, Stainless’s language currently does not provide a default encoding of e.g. concurrency with a shared mutable heap, though it might support more manageable forms of concurrency in the future.

If you would like to use Stainless now, check the Getting Started section and try our Tutorial. To learn more about the functionality that Stainless provides, read on below.

## Software Verification¶

The Stainless program verifier collects a list of top-level functions,
and verifies the *validity* of their *contracts*. Essentially, for each function,
it will (try to) prove that the postcondition always holds, assuming a given
precondition does hold. A simple example:

```
def factorial(n: BigInt): BigInt = {
require(n >= 0)
if(n == 0) {
BigInt(1)
} else {
n * factorial(n - 1)
}
} ensuring(res => res >= 0)
```

Stainless generates a `postcondition`

verification condition for the above
function, corresponding to the predicate parameter to the `ensuring`

expression. It attempts to prove it using a combination of an internal
algorithm and external automated theorem proving. Stainless will return one of the
following:

- The postcondition is
`valid`

. In that case, Stainless was able to prove that for**any**input to the function satisfying the precondition, the postcondition will always hold. - The postcondition is
`invalid`

. It means that Stainless disproved the postcondition and that there exists at least one input satisfying the precondition such that the postcondition does not hold. Stainless will always return a concrete counterexample, very useful when trying to understand why a function is not satisfying its contract. - The postcondition is
`unknown`

. It means Stainless is unable to prove or find a counterexample. It usually happens after a timeout or an internal error occurring in the external theorem prover.

Stainless will also verify for each call site that the precondition of the invoked function cannot be violated.

Stainless supports verification of a significant part of the Scala language, described in Pure Scala and Imperative.

## Program Termination¶

A “verified” function in stainless is guaranteed to never crash, however, it can still lead to an infinite evaluation. Stainless therefore provides a termination checker that complements the verification of safety properties.

For each function in the program, Stainless will try to automatically infer a decreasing metric associated with this function to prove termination. The termination checker will then report one of the following:

- The function
`terminates`

. In this case, Stainless was able to prove that for all inputs (satisfying the function’s precondition), evaluation of the function under those inputs is guaranteed to terminate. - The function
`loops`

. In this case, Stainless was able to construct an input to the function such that evaluation under that input will be looping. - The function
`maybe loops`

. In the case where recursive functions are passed around as first-class functions, Stainless will sometimes over-approximate the potential call sites and report loops that may never occur. - Termination of the function is
`unknown`

. In this case, Stainless was neither able to prove nor disprove termination of the relevant function. Automated termination proving is a*hard*problem and such cases are thus to be expected.

In cases where automated termination checking fails, Stainless provides the user
with the ability to manually specify a measure under which termination should
occur through the `decreases`

construct. For example, the
McCarthy 91 function
can be shown terminating as follows:

```
def M(n: BigInt): BigInt = {
decreases(stainless.math.max(101 - n, 0))
if (n > 100) n - 10 else M(M(n + 11))
} ensuring (_ == (if (n > 100) n - 10 else BigInt(91)))
```

It is also possible to add a pre-condition (`require(...)`

) *before* `decreases`

.