Stainless Documentation
Contents
|
Introduction
Stainless documentation
¶
Contents:
Introduction
Stainless and Scala
Software Verification
Program Termination
Getting Started
Installing Stainless
sbt
Linux & Mac OS-X
Windows
External Solvers
Running Tests
Building Stainless Documentation
Using Stainless in Eclipse
Tutorial: Sorting
Warm-up: Max
Defining Lists and Their Properties
Insertion into Sorted List
Being Sorted is Not Enough
Using Size in Specification
Using Content in Specification
Pure Scala
Boolean
TupleX
Int
BigInt
Real
Set
Functional Array
Map
Function
Stainless Library
Annotations
List[T]
Set[T], Map[T]
Imperative
Imperative Code
While loops
Arrays
Mutable Objects
Aliasing
Annotations for Imperative Programming
Verification
Verification conditions
Proving Theorems
A practical introduction to proofs
Techniques for proving non-trivial propositions
Techniques for proving non-trivial postconditions
A complex example: additivity of measures
Quick Recap
Limitations of Verification
Out of Memory Errors
Command Line Options
Choosing which Stainless feature to use
Additional top-level options
Additional Options (by component)
Stainless Smart Contracts
Overview
Installation
Formal Verification of Smart Contracts
Compilation to Solidity
Features
Development
Known Issues
Reporting Issues
Frequently Asked Questions
Proving properties of size
Compiling Stainless programs to bytecode
References
Videos
Papers
Books
Stainless’ Internals
Search Page
Table Of Contents
Introduction
Getting Started
Installing Stainless
Tutorial: Sorting
Pure Scala
Stainless Library
Imperative
Verification
Proving Theorems
Limitations of Verification
Command Line Options
Stainless Smart Contracts
Frequently Asked Questions
References
Stainless’ Internals