The Why3 Platform¶
- Authors
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
- Version
1.5, April 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
- 2. Getting Started
- 3. Why3 by Examples
- 4. The Why3 API
- 5. Compilation, Installation
- 6. Reference Manuals for the Why3 Tools
- 7. The WhyML Language Reference
- 8. The VC Generators
- 9. Other Input Formats
- 10. Executing WhyML Programs
- 11. Interactive Proof Assistants
- 12. Technical Informations
- 12.1. Structure of Session Files
- 12.2. Prover Detection
- 12.3. The
why3.conf
Configuration File - 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
- 14. Bibliography
- 15. Index