README.md 1.76 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2
WHY3
====
MARCHE Claude's avatar
MARCHE Claude committed
3

4 5 6 7 8 9 10 11 12 13
Why3 is a platform for deductive program verification. It provides
a rich language for specification and programming, called WhyML, and
relies on external theorem provers, both automated and interactive,
to discharge verification conditions. Why3 comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data structures
(arrays, queues, hash tables, etc.). A user can write WhyML programs
directly and get correct-by-construction OCaml programs through an
automated extraction mechanism. WhyML is also used as an intermediate
language for the verification of C, Java, or Ada programs.
MARCHE Claude's avatar
MARCHE Claude committed
14

MARCHE Claude's avatar
MARCHE Claude committed
15
PROJECT HOME
16
------------
MARCHE Claude's avatar
MARCHE Claude committed
17

18
http://why3.lri.fr/
19

20
https://gitlab.inria.fr/why3/why3
MARCHE Claude's avatar
MARCHE Claude committed
21

MARCHE Claude's avatar
MARCHE Claude committed
22
DOCUMENTATION
23
-------------
MARCHE Claude's avatar
MARCHE Claude committed
24

25 26 27
The documentation (a tutorial and a reference manual) is in the file
[doc/manual.pdf](http://why3.lri.fr/manual.pdf) or online at
http://why3.lri.fr/doc/.
MARCHE Claude's avatar
MARCHE Claude committed
28

29
Various examples can be found in the subdirectories [stdlib/](stdlib)
30
and [examples/](examples).
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34 35

Mailing list (Why3 Club):
  http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Bug Tracking System:
36
  https://gitlab.inria.fr/why3/why3/issues
MARCHE Claude's avatar
MARCHE Claude committed
37 38

COPYRIGHT
39
---------
MARCHE Claude's avatar
MARCHE Claude committed
40 41

This program is distributed under the GNU LGPL 2.1. See the enclosed
42
file [LICENSE](LICENSE).
MARCHE Claude's avatar
MARCHE Claude committed
43

44 45 46
The files [src/util/extmap.ml{i}](src/util/extmap.mli) are derived from the
sources of OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file [OCAML-LICENSE](OCAML-LICENSE)).
MARCHE Claude's avatar
MARCHE Claude committed
47

48 49
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
50
licenses are detailed in files [share/images/\*/\*.txt](share/images).
51

MARCHE Claude's avatar
MARCHE Claude committed
52
INSTALLATION
53
------------
MARCHE Claude's avatar
MARCHE Claude committed
54

55
See the file [INSTALL.md](INSTALL.md).