Stainless documentation

Contents:

• Introduction
  • Stainless and Scala
  • Software Verification
  • Program Termination
• Installing Stainless
  • General Requirement
  • Obtain From A Package Manager
  • Github Codespaces
  • Use Standalone Release
  • Usage Within An Existing Project
  • Running Code with Stainless dependencies
  • External Solver Binaries
  • Build from Source on Linux & macOS
  • Build from Source on Windows
  • Running Tests
  • Building Stainless Documentation
  • Using IDEs with –no-colors option. Emacs illustration
• Verifying and Compiling Examples
  • Verifying Examples
  • Compiling and Executing Examples
• 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
• Specifying Options
  • Choosing which Stainless feature to use
  • Additional top-level options
  • Additional Options (by component)
  • Configuration File
  • Library Files
• Verification conditions
  • Postconditions
  • Preconditions
  • Sharing bindings between specifications and function body
  • Loop invariants
  • Decrease annotation in loops
  • Array access safety
  • ADT invariants
  • Pattern matching exhaustiveness
• Specifying Algebraic Properties
  • Introduction
  • Typeclasses
  • Typeclass inheritance
  • Associated methods
  • Coherence
  • Under the hood
• Imperative and Other Effects
  • Imperative Code
  • While loops
  • Arrays
  • Mutable Objects
  • Aliasing
  • Annotations for Imperative Programming
  • Extern functions and abstract methods
  • Trait Variables
  • Return keyword
  • Exceptions
• Equivalence Checking
  • Example run
• Ghost Context
  • Introduction
  • Ghost annotation
  • Correctness check
  • Ghost expression elimination
  • Case study
• Working With Existing Code
  • A wrapper for TrieMap
  • Extern methods
  • Contracts
  • Purity annotations
• Pure Scala
  • Booleans
  • Algebraic Data Types
  • Generics
  • Methods
  • Type Definitions
  • Specifications
  • Expressions
  • Predefined Types
• Stainless Library
  • Annotations
  • List[T]
  • Set[T], Map[T]
  • PartialFunction[A, B]
• Generating C Code
  • Requirements
  • Export
  • Supported Features
  • Global State
  • Custom Conversion
  • API For Safe Low Level Programs
• 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
• Case Studies
  • Case Study #1: Proving invariants of actor systems
• Translation from Stainless to Coq
  • Requirements
  • Usage of the Coq option
• FAQ: (Frequently) Asked Questions
  • How does Stainless compare to other verification tools?
  • How does Stainless compare to fuzzing tools?
  • Does Stainless use SMT solvers?
  • What are the conditions required for Stainless to be applied to industry software?
  • Can I use Stainless with Java?
  • Can I use Stainless with Rust?
  • Proving properties of size
  • Compiling Stainless programs to bytecode
• References
  • Videos
  • Papers
  • Books
• Stainless’ Internals

• Search Page