The Why3 Platform

Authors:

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

Version:

1.7, April 2024

Copyright:

2010–2024 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. Compilation, Installation
  • 4.1. Installing Why3
    • 4.1.1. Installation via Opam
    • 4.1.2. Installation via Docker
    • 4.1.3. Installation from sources
  • 4.2. Installing External Provers
    • 4.2.1. Multiple versions of the same prover
    • 4.2.2. Session update after prover upgrade
  • 4.3. Editing WhyML Sources
    • 4.3.1. Emacs
    • 4.3.2. Vim
  • 4.4. Shells Auto-completion for Why3
  • 4.5. Inference of Loop Invariants
• 5. The Why3 Tools
  • 5.1. The config Command
    • 5.1.1. Command add-prover
    • 5.1.2. Command detect
    • 5.1.3. Command list-provers
    • 5.1.4. Command list-supported-provers
    • 5.1.5. Command show
  • 5.2. The prove Command
    • 5.2.1. Prover Results
    • 5.2.2. Options
    • 5.2.3. Generating potential counterexamples
    • 5.2.4. Generating validated and categorized counterexamples
  • 5.3. The ide Command
    • 5.3.1. Session
    • 5.3.2. Context Menu
    • 5.3.3. Global Menus
    • 5.3.4. Command-line interface
    • 5.3.5. Key shortcuts
    • 5.3.6. Preferences Dialog
    • 5.3.7. Displaying Counterexamples
  • 5.4. The replay Command
    • 5.4.1. Obsolete proofs
    • 5.4.2. Exit code and options
    • 5.4.3. Smoke detector
  • 5.5. The session Command
    • 5.5.1. Command info
    • 5.5.2. Command latex
    • 5.5.3. Command html
    • 5.5.4. Command update
    • 5.5.5. Command create
  • 5.6. The doc Command
    • 5.6.1. Options
    • 5.6.2. Typesetting textual comments
  • 5.7. The pp Command
  • 5.8. The execute Command
    • 5.8.1. Runtime assertion checking (RAC)
    • 5.8.2. Options
  • 5.9. The extract Command
  • 5.10. The realize Command
  • 5.11. The show Command
    • 5.11.1. Command attributes
    • 5.11.2. Command formats
    • 5.11.3. Command metas
    • 5.11.4. Command printers
    • 5.11.5. Command transformations
  • 5.12. The wc Command
  • 5.13. The bench Command
• 6. The WhyML Language Reference
  • 6.1. Lexical Conventions
  • 6.2. Type Expressions
  • 6.3. Logical Expressions
    • 6.3.1. Terms and formulas
    • 6.3.2. Specific syntax for collections
    • 6.3.3. The “at” and “old” operators
    • 6.3.4. Non-standard connectives
    • 6.3.5. Conditionals, “let” bindings and pattern-matching
  • 6.4. Program Expressions
    • 6.4.1. Ghost expressions
    • 6.4.2. Assignment expressions
    • 6.4.3. Auto-dereference: simplified usage of mutable variables
    • 6.4.4. Evaluation order
    • 6.4.5. The “for” loop
    • 6.4.6. The “for each” loop
    • 6.4.7. Break & Continue
    • 6.4.8. Function literals
    • 6.4.9. The any expression
  • 6.5. Modules
    • 6.5.1. Record types
    • 6.5.2. Algebraic data types
    • 6.5.3. Range types
    • 6.5.4. Floating-point types
    • 6.5.5. Function declarations
    • 6.5.6. Module cloning
    • 6.5.7. Module interface
  • 6.6. The Why3 Standard Library
    • 6.6.1. Library int: mathematical integers
    • 6.6.2. Library array: array data structure
• 7. Other Input Formats
  • 7.1. micro-C
    • 7.1.1. Syntax of micro-C
    • 7.1.2. Built-in functions and predicates
  • 7.2. micro-Python
    • 7.2.1. Syntax of micro-Python
    • 7.2.2. Built-in functions and predicates
    • 7.2.3. Limitations
  • 7.3. MLCFG
    • 7.3.1. Syntax of the MLCFG language
    • 7.3.2. An example
    • 7.3.3. Error messages
    • 7.3.4. Current limitations
    • 7.3.5. Alternative translation scheme: Stackify
    • 7.3.6. Subregion analysis
  • 7.4. S-expressions
  • 7.5. Coma
• 8. The VC Generators
  • 8.1. Program Functions
  • 8.2. Controlling the VC generation
    • 8.2.1. Reducing size of VCs using Strongest Postconditions
    • 8.2.2. Ignoring checks for termination
    • 8.2.3. Using a custom well-founded relation for termination
    • 8.2.4. Keeping preconditions of calls in the logical context
  • 8.3. Type Invariants
  • 8.4. Lemma Functions
  • 8.5. Automatic Inference of Loop Invariants
    • 8.5.1. Current limitations
• 9. Executing WhyML Programs
  • 9.1. Interpreting WhyML Code
  • 9.2. Compiling WhyML to OCaml
    • 9.2.1. Examples
    • 9.2.2. Extraction of functors
    • 9.2.3. Custom extraction drivers
  • 9.3. Compiling to Other Languages
    • 9.3.1. Compiling to C
• 10. Interactive Proof Assistants
  • 10.1. Using an Interactive Proof Assistant to Discharge Goals
  • 10.2. Theory Realizations
    • 10.2.1. Generating a realization
    • 10.2.2. Using realizations inside proofs
    • 10.2.3. Shipping libraries of realizations
  • 10.3. Coq
  • 10.4. Isabelle/HOL
    • 10.4.1. Installation
    • 10.4.2. Usage
    • 10.4.3. Using Isabelle server
    • 10.4.4. Realizations
  • 10.5. PVS
    • 10.5.1. Installation
    • 10.5.2. Usage
    • 10.5.3. Realization
• 11. The Why3 API
  • 11.1. Building Propositional Formulas
  • 11.2. Building Tasks
  • 11.3. Calling External Provers
  • 11.4. Building Terms
  • 11.5. Building Quantified Formulas
  • 11.6. Building Theories
  • 11.7. Operations on Terms and Formulas, Transformations
  • 11.8. Proof Sessions
  • 11.9. ML Programs
    • 11.9.1. Untyped syntax tree
    • 11.9.2. Alternative, top-down, construction of parsing trees
    • 11.9.3. Using the parsing trees
    • 11.9.4. Use attributes to infer loop invariants
    • 11.9.5. Typed declaration
  • 11.10. Generating Counterexamples
    • 11.10.1. Attributes and locations on identifiers
    • 11.10.2. Attributes in formulas
    • 11.10.3. Counterexamples output formats
    • 11.10.4. Checking counterexamples
• 12. Technical Informations
  • 12.1. Prover Detection
  • 12.2. The why3.conf Configuration File
    • 12.2.1. Extra configuration files
  • 12.3. Drivers for External Provers
  • 12.4. Drivers for User Theories
  • 12.5. Transformations
  • 12.6. Proof Strategies
    • 12.6.1. Basic Strategies
    • 12.6.2. Forward propagation in floating-point computations
  • 12.7. WhyML Attributes
  • 12.8. Why3 Metas
  • 12.9. Debug Flags
  • 12.10. Structure of Session Files
  • 12.11. Structure of Counterexamples
  • 12.12. Developer Documentation
    • 12.12.1. Updating messages for syntax errors
• 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
• Index