doc/foreword.rst

   1 Foreword
   2 ========
   3
   4 Why3 is a platform for deductive program verification. It provides a
   5 rich language for specification and programming, called WhyML, and
   6 relies on external theorem provers, both automated and interactive, to
   7 discharge verification conditions. Why3 comes with a standard library of
   8 logical theories (integer and real arithmetic, Boolean operations, sets
   9 and maps, etc.) and basic programming data structures (arrays, queues,
  10 hash tables, etc.). A user can write WhyML programs directly and get
  11 correct-by-construction OCaml programs through an automated extraction
  12 mechanism. WhyML is also used as an intermediate language for the
  13 verification of C, Java, or Ada programs.
  14
  15 Why3 is a complete reimplementation of the former Why
  16 platform :cite:`filliatre07cav`. Among the new features are:
  17 numerous extensions to the input language, a new architecture for
  18 calling external provers, and a well-designed API, allowing to use Why3
  19 as a software library. An important emphasis is put on modularity and
  20 genericity, giving the end user a possibility to easily reuse Why3
  21 formalizations or to add support for a new external prover if wanted.
  22
  23 Availability
  24 ~~~~~~~~~~~~
  25
  26 Why3 project page is https://www.why3.org/. The latest release is
  27 available there, in source format, together with this documentation and
  28 several examples.
  29
  30 Why3 is also distributed under the form of an OPAM package and a Debian
  31 package.
  32
  33 Why3 is distributed as open source and freely available under the terms
  34 of the GNU LGPL 2.1. See the file :file:`LICENSE`.
  35
  36 See the file :file:`INSTALL.md` for quick installation instructions, and
  37 :numref:`sec.install` of this document for more detailed instructions.
  38
  39 Contact
  40 ~~~~~~~
  41
  42 There is a public mailing list for users’ discussions:
  43 https://groupes.renater.fr/sympa/info/why3-club.
  44
  45 Report any bug to the Why3 Bug Tracking System:
  46 https://gitlab.inria.fr/why3/why3/issues.
  47
  48 Acknowledgements
  49 ~~~~~~~~~~~~~~~~
  50
  51 We gratefully thank the people who contributed to Why3, directly or
  52 indirectly: Stefan Berghofer, Sylvie Boldo, Martin Clochard, Simon
  53 Cruanes, Sylvain Dailler, Xavier Denis, Clément Fumex, Léon Gondelman, David Hauzar,
  54 Daisuke Ishii, Jacques-Henri Jourdan, Johannes Kanig, Mikhail Mandrykin, David Mentré, Benjamin
  55 Monate, Kim Nguyen, Thi-Minh-Tuyen Nguyen, Mário Pereira, Raphaël
  56 Rieu-Helft, Simāo Melo de Sousa, Asma Tafat, Piotr Trojanek, Makarius
  57 Wenzel.