README.md

   1 WHY3
   2 ====
   3
   4 Why3 is a platform for deductive program verification. It provides
   5 a rich language for specification and programming, called WhyML, and
   6 relies on external theorem provers, both automated and interactive,
   7 to discharge verification conditions. Why3 comes with a standard
   8 library of logical theories (integer and real arithmetic, Boolean
   9 operations, sets and maps, etc.) and basic programming data structures
  10 (arrays, queues, hash tables, etc.). A user can write WhyML programs
  11 directly and get correct-by-construction OCaml programs through an
  12 automated extraction mechanism. WhyML is also used as an intermediate
  13 language for the verification of C, Java, or Ada programs.
  14
  15 PROJECT HOME
  16 ------------
  17
  18 https://www.why3.org/
  19
  20 https://gitlab.inria.fr/why3/why3
  21
  22 DOCUMENTATION
  23 -------------
  24
  25 The documentation (a tutorial and a reference manual) is
  26 available [online](https://www.why3.org/doc/).
  27
  28 Various examples can be found in the subdirectories [stdlib/](stdlib)
  29 and [examples/](examples).
  30
  31 COPYRIGHT
  32 ---------
  33
  34 This program is distributed under the GNU LGPL 2.1. See the enclosed
  35 file [LICENSE](LICENSE).
  36
  37 The files [src/util/extmap.ml{i}](src/util/extmap.mli) are derived from the
  38 sources of OCaml 3.12 standard library, and are distributed under the GNU
  39 LGPL version 2 (see file [OCAML-LICENSE](OCAML-LICENSE)).
  40
  41 Icon sets for the graphical interface of Why3 are subject to specific
  42 licenses, some of them may forbid commercial usage. These specific
  43 licenses are detailed in files [share/images/\*/\*.txt](share/images).
  44
  45 INSTALLATION
  46 ------------
  47
  48 See the file [INSTALL.md](INSTALL.md).