Certora Prover Documentation
74

Contents

  • Certora Technology White Paper
  • Certora User’s Guide
  • The Certora Verification Language
  • The Certora Prover
  • Gambit: Mutation Generator for Solidity
  • Equivalence Checking Using the Certora Prover
  • Old Documentation
    • Specification By Example
      • The Bank
      • The (Iterable) Map
        • Overview
        • A Simple Map
        • The IterableMap Contract
        • Verification With Ghosts
    • The Anatomy of a Specification
    • Advanced Subjects
    • Best Practices
    • Common Pitfalls
    • Assert splitting
    • Troubleshooting
Certora Prover Documentation
  • »
  • Old Documentation »
  • Specification By Example »
  • The (Iterable) Map
  • Edit on GitHub

Warning

This page was created from a pull request (#74).

The (Iterable) Map

  • Overview
  • A Simple Map
    • The code
    • Writing specs
      • Generalized unit tests
      • Revert conditions
      • Inverses
  • The IterableMap Contract
    • Adding iteration
    • A soft introduction to ghosts
  • Verification With Ghosts
Previous Next

© Copyright 2022, Certora, Inc. Revision be21c3fb.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: 74
Versions
latest
cvl1
Downloads
On Read the Docs
Project Home
Builds