The Why3 Platform

Authors

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich

Version

1.5, September 2022

Copyright

2010–2022 University Paris-Saclay, CNRS, Inria

This work has been partly supported by the U3CAT national ANR project (ANR-08-SEGI-021-08), the Hi-Lite FUI project of the System@tic competitivity cluster, the BWare ANR project (ANR-12-INSE-0010), the Joint Laboratory ProofInUse (ANR-13-LAB3-0007), the CoLiS ANR project (ANR-15-CE25-0001), and the VOCaL ANR project (ANR-15-CE25-008).

• 1. Foreword
  • 1.1. Availability
  • 1.2. Contact
  • 1.3. Acknowledgements
• 2. Getting Started
  • 2.1. Hello Proofs
  • 2.2. Getting Started with the GUI
    • 2.2.1. Calling provers on goals
    • 2.2.2. Applying transformations
    • 2.2.3. Modifying the input
    • 2.2.4. Replaying obsolete proofs
    • 2.2.5. Cleaning
  • 2.3. Getting Started with the Why3 Command
• 3. Why3 by Examples
  • 3.1. Problem 0: Einstein’s Problem
  • 3.2. Problem 1: Sum and Maximum
  • 3.3. Problem 2: Inverting an Injection
  • 3.4. Problem 3: Searching a Linked List
  • 3.5. Problem 4: N-Queens
  • 3.6. Problem 5: Amortized Queue
• 4. The Why3 API
  • 4.1. Building Propositional Formulas
  • 4.2. Building Tasks
  • 4.3. Calling External Provers
  • 4.4. Building Terms
  • 4.5. Building Quantified Formulas
  • 4.6. Building Theories
  • 4.7. Operations on Terms and Formulas, Transformations
  • 4.8. Proof Sessions
  • 4.9. ML Programs
    • 4.9.1. Untyped syntax tree
    • 4.9.2. Alternative, top-down, construction of parsing trees
    • 4.9.3. Using the parsing trees
    • 4.9.4. Use attributes to infer loop invariants
    • 4.9.5. Typed declaration
  • 4.10. Generating counterexamples
    • 4.10.1. Attributes and locations on identifiers
    • 4.10.2. Attributes in formulas
    • 4.10.3. Counterexamples output formats
    • 4.10.4. Checking counterexamples
• 5. Compilation, Installation
  • 5.1. Installing Why3
    • 5.1.1. Installation via Opam
    • 5.1.2. Installation via Docker
    • 5.1.3. Installation from Source Distribution
  • 5.2. Installing External Provers
    • 5.2.1. Multiple Versions of the Same Prover
    • 5.2.2. Session Update after Prover Upgrade
  • 5.3. Configure Editors for editing WhyML sources
    • 5.3.1. Emacs
    • 5.3.2. Vim
  • 5.4. Configure Shells for auto-completion of Why3 command arguments
  • 5.5. Inference of Loop Invariants
• 6. Reference Manuals for the Why3 Tools
  • 6.1. The config Command
    • 6.1.1. Command add-prover
    • 6.1.2. Command detect
    • 6.1.3. Command list-provers
    • 6.1.4. Command list-supported-provers
    • 6.1.5. Command show
  • 6.2. The prove Command
    • 6.2.1. Prover Results
    • 6.2.2. Options
    • 6.2.3. Generating potential counterexamples
    • 6.2.4. Generating validated and categorized counterexamples
  • 6.3. The ide Command
    • 6.3.1. Session
    • 6.3.2. Context Menu
    • 6.3.3. Global Menus
    • 6.3.4. Command-line interface
    • 6.3.5. Key shortcuts
    • 6.3.6. Preferences Dialog
    • 6.3.7. Displaying Counterexamples
  • 6.4. The replay Command
    • 6.4.1. Obsolete proofs
    • 6.4.2. Exit code and options
    • 6.4.3. Smoke detector
  • 6.5. The session Command
    • 6.5.1. Command info
    • 6.5.2. Command latex
    • 6.5.3. Command html
    • 6.5.4. Command update
  • 6.6. The doc Command
    • 6.6.1. Options
    • 6.6.2. Typesetting textual comments
  • 6.7. The pp Command
  • 6.8. The execute Command
    • 6.8.1. Runtime assertion checking (RAC)
    • 6.8.2. Options
  • 6.9. The extract Command
  • 6.10. The realize Command
  • 6.11. The show Command
    • 6.11.1. Command attributes
    • 6.11.2. Command formats
    • 6.11.3. Command metas
    • 6.11.4. Command printers
    • 6.11.5. Command transformations
  • 6.12. The wc Command
• 7. The WhyML Language Reference
  • 7.1. Lexical Conventions
  • 7.2. Type expressions
  • 7.3. Logical expressions
    • 7.3.1. Terms and Formulas
    • 7.3.2. Specific syntax for collections
    • 7.3.3. The “at” and “old” operators
    • 7.3.4. Non-standard connectives
    • 7.3.5. Conditionals, “let” bindings and pattern-matching
  • 7.4. Program expressions
    • 7.4.1. Ghost expressions
    • 7.4.2. Assignment expressions
    • 7.4.3. Auto-dereference: simplified usage of mutable variables
    • 7.4.4. Evaluation order
    • 7.4.5. The “for” loop
    • 7.4.6. The “for each” loop
    • 7.4.7. Break & Continue
    • 7.4.8. Function literals
    • 7.4.9. The any expression
  • 7.5. Modules
    • 7.5.1. Record types
    • 7.5.2. Algebraic data types
    • 7.5.3. Range types
    • 7.5.4. Floating-point types
    • 7.5.5. Function declarations
    • 7.5.6. Module cloning
  • 7.6. The Why3 Standard Library
    • 7.6.1. Library int: mathematical integers
    • 7.6.2. Library array: array data structure
• 8. The VC Generators
  • 8.1. VC generation for program functions
  • 8.2. VC generated for type invariants
  • 8.3. VC generation and lemma functions
  • 8.4. Using strongest post-conditions
  • 8.5. Automatic inference of loop invariants
    • 8.5.1. Current limitations
• 9. Other Input Formats
  • 9.1. micro-C
    • 9.1.1. Syntax of micro-C
    • 9.1.2. Built-in functions and predicates
  • 9.2. micro-Python
    • 9.2.1. Syntax of micro-Python
    • 9.2.2. Built-in functions and predicates
    • 9.2.3. Limitations
  • 9.3. MLCFG: function bodies in the style of control-flow graphs
    • 9.3.1. Syntax of the MLCFG language
    • 9.3.2. An example
    • 9.3.3. Error messages
    • 9.3.4. Current limitations
• 10. Executing WhyML Programs
  • 10.1. Interpreting WhyML Code
  • 10.2. Compiling WhyML to OCaml
    • 10.2.1. Examples
    • 10.2.2. Extraction of Functors
    • 10.2.3. Custom Extraction Drivers
• 11. Interactive Proof Assistants
  • 11.1. Using an Interactive Proof Assistant to Discharge Goals
  • 11.2. Theory Realizations
    • 11.2.1. Generating a realization
    • 11.2.2. Using realizations inside proofs
    • 11.2.3. Shipping libraries of realizations
  • 11.3. Coq
  • 11.4. Isabelle/HOL
    • 11.4.1. Installation
    • 11.4.2. Usage
    • 11.4.3. Using Isabelle server
    • 11.4.4. Realizations
  • 11.5. PVS
    • 11.5.1. Installation
    • 11.5.2. Usage
    • 11.5.3. Realization
• 12. Technical Informations
  • 12.1. Structure of Session Files
  • 12.2. Prover Detection
  • 12.3. The why3.conf Configuration File
    • 12.3.1. Extra Configuration Files
  • 12.4. Drivers for External Provers
  • 12.5. Adding extra drivers for user theories
  • 12.6. Transformations
  • 12.7. Proof Strategies
  • 12.8. WhyML Attributes
  • 12.9. Why3 Metas
  • 12.10. Debug Flags
  • 12.11. Updating Syntax Error Messages
• 13. Release Notes
  • 13.1. Release Notes for version 1.2: new syntax for “auto-dereference”
  • 13.2. Release Notes for version 1.0: syntax changes w.r.t. 0.88
  • 13.3. Release Notes for version 0.80: syntax changes w.r.t. 0.73
  • 13.4. Summary of Changes w.r.t. Why 2
• 14. Bibliography
• 15. Index