README 1.42 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2 3 4 5 6 7 8 9 10 11
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
12

MARCHE Claude's avatar
MARCHE Claude committed
13 14 15
PROJECT HOME
============

16 17
http://why3.lri.fr

MARCHE Claude's avatar
MARCHE Claude committed
18 19
https://gforge.inria.fr/projects/why3

MARCHE Claude's avatar
MARCHE Claude committed
20 21 22 23 24 25
DOCUMENTATION
=============

The documentation (a tutorial and a reference manual) is in
the file doc/manual.pdf.

Andrei Paskevich's avatar
Andrei Paskevich committed
26 27
Various examples can be found in the subdirectories theories/
and examples/.
MARCHE Claude's avatar
MARCHE Claude committed
28 29 30 31 32 33 34 35 36 37 38 39 40

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

Bug Tracking System:
  https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse

COPYRIGHT
=========

This program is distributed under the GNU LGPL 2.1. See the enclosed
file LICENSE.

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

INSTALLATION
============

MARCHE Claude's avatar
MARCHE Claude committed
48
See the file INSTALL.