Stainless Library¶
Stainless defines its own library with some core data types and
operations on them, which work with the fragment supported
by Stainless, available in frontends/library/stainless
, which
we encourage the reader to consult as it is always up to date.
One of the reasons for a separate library is to
ensure that these operations can be correctly mapped to
mathematical functions and relations inside of SMT solvers,
largely defined by the SMTLIB standard (see
http://www.smtlib.org/). Thus for some data types, such as
BigInt
, Stainless provides a dedicated mapping to support reasoning.
(If you are a fan
of growing the language only through libraries, keep in mind that
growing operations together with the ability to reason about them
is what the development of mathematical theories is all about, and
is a process slower than putting together
libraries of unverified code–efficient automation of reasoning about a
single decidable theory generally results in multiple research papers.)
For other operations (e.g., List[T]), the library
is much like Stainless userdefined code, but specifies some
useful preconditions and postconditions of the operations, thus
providing reasoning abilities using mechanisms entirely available
to the user.
Note
The ScalaDoc for the library is available online.
For the most uptodate version of the source code of library,
please consult the library/
directory in your Stainless distribution.
To use Stainless’ libraries, you need to use the appropriate import directive at the top of Stainless’ compilation units. Here is a quick summary of what to import.
Package to import 
What it gives access to 

stainless.annotation._ 
Stainless annotations, e.g. @induct 
stainless.lang._ 
Map, Set, PartialFunction, holds, passes, invariant 
stainless.collection._ 
List[T] and subclasses, Option[T] and subclasses 
To learn more, we encourage you to look in the library/ subdirectory of Stainless distribution.
Annotations¶
Stainless provides some special annotations in the package stainless.annotation
,
which instruct Stainless to handle some functions or objects in a specialized way.
Annotation 
Meaning 


Treat this object/function as library, don’t try
to verify its specification. Can be overridden by
including a function name in the 

Use the inductive tactic when generating verification conditions. 

Treat the annotated method as an invariant of the enclosing
class. Can be used instead of 

Drop the annotated field or method during compilation. See the corresponding section for more information. 

Only extract the contracts of a function, replacing
its body by a 

Used to hide a function 

Do not generate verification conditions for this function. 

Specify that this function is pure, which will then
be checked. If the function is also annotated with


Ignore this definition when extracting Stainless trees. This annotation is useful to define functions that are not in Stainless’s language but will be hardcoded into specialized trees, or to include code written in full Scala which is not verifiable by Stainless. Can also be used on class fields whose type cannot be understood by Stainless, eg. because it comes from an external library, the JDK, or some other code which does not understand. See the corresponding documentation page. 

Inline this function. Stainless will refuse to inline (mutually) recursive functions. 

Inline this function but only once, which is allowed even on (mutually) recursive functions. Note: A recursive function will not be inlined within itself. 

Partially evaluate calls to this function.
Note: 
Stainless also has some special keywords defined in stainless.lang
that can be used around
function calls. Here is an example for unfold
.
Annotation 
Meaning 


Callsite inlining 

Inject an equality assumption between a function call and its
unfolded version. Can be useful to locally override an

List[T]¶
As there is no special support for Lists in SMT solvers, Stainless Lists are encoded as an ordinary algebraic data type:
sealed abstract class List[T]
case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]
List API¶
Stainless Lists support a rich and strongly specified API.
Method signature for 
Short description 


Number of elements in this List. 

The set of elements in this List. 

Returns true if this List contains 

Append this List with 

Returns the head of this List. Can only be called on a nonempty List. 

Returns the tail of this List. Can only be called on a nonempty List. 

Return the element in index 

Prepend an element to this List. 

Append an element to this List. 

The reverse of this List. 

Take the first 

This List without the first 

Take a sublist of this List, from index 

Replace all occurrences of 



Zip this list with 

Remove all occurrences of 

Remove all occurrences of any element in 

A list of all elements that occur both in


Add 

Look for the element 

Return this List except for the last element. Can only be called on nonempty Lists. 

Return the last element of this List. Can only be called on nonempty Lists. 

Optionally return the last element of this List. 

Optionally return the first element of this List. 

Return this List without duplicates. 

Split this List to chunks separated by an
occurrence of 

Split this List in chunks separated by an
occurrence of any element in 

Count the occurrences of 

Split this List in two halves. 

Insert an element after index 

Replace the 

Rotate this list by 

Returns whether this List is empty. 

Builds a new List by applying a predicate 

Applies the binary operator 

Applies a binary operator 

Produces a List containing cumulative results
of applying the operator 

Produces a List containing cumulative results
of applying the operator 

Builds a new List by applying a function 

Selects all elements of this List
which satisfy the predicate 

Tests whether predicate 

Tests whether predicate 

Finds the first element of this List satisfying
predicate 

Takes longest prefix of elements that satisfy
predicate 
Additional operations on Lists¶
The object ListOps
offers this additional operations:
Function signature 
Short description 


Converts the List of Lists 

Returns whether this list of mathematical integers is sorted in ascending order. 

Sorts this list of mathematical integers is sorted in ascending order. 

Sorts this list of mathematical integers is sorted in ascending order using insertion sort. 
Theorems on Lists¶
The following theorems on Lists have been proven by Stainless and are included
in the object ListSpecs
:
Theorem signature 
Proven Claim 



















Set[T], Map[T]¶
Stainless uses its own Sets and Maps, which are defined in the stainless.lang
package.
However, these classes are not implemented within Stainless.
Instead, they are parsed into specialized trees.
Methods of these classes are mapped to specialized trees within SMT solvers.
For code generation, we rely on Java Sets and Maps.
The API of these classes is a subset of the Scala API and can be found in the Pure Scala section.
Additionally, the following functions for Sets are provided in the
stainless.collection
package:
Function signature 
Short description 


Transforms the Set 

Tests whether predicate 

Tests whether predicate 
PartialFunction[A, B]¶
To define anonymous functions with preconditions, Stainless has a PartialFunction[A, B]
type
with the corresponding annotation A ~> B
. To construct a partial function, you must use
PartialFunction.apply
as in the unOpt
function below. The precondition written in the
require
becomes the pre
field of the partial function (as in the call to f.pre
in map1
).
def map1[A, B](l: List[A], f: A ~> B): List[B] = {
require(l.forall(f.pre))
l match {
case Cons(x, xs) => Cons[B](f(x), map1(xs, f))
case Nil() => Nil[B]()
}
}
def unOpt[T](l: List[Option[T]]): List[T] = {
require(l.forall(_.nonEmpty))
map1(l, PartialFunction {(x:Option[T]) => require(x.nonEmpty); x.get})
}
Partial functions can also be written using pattern matching:
def unOptCase[T](l: List[Option[T]]): List[T] = {
require(l.forall { case Some(_) => true; case _ => false })
map1(l, PartialFunction[Option[T], T] { case Some(v) => v })
}