README 952 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6


Why3 is a tool for automated and interactive proving in first-order
polymorphic logic. It provides a collection of command-line tools, a
graphical interface and an Objective Caml library.

MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11
PROJECT HOME
============

https://gforge.inria.fr/projects/why3

MARCHE Claude's avatar
MARCHE Claude committed
12 13 14 15 16 17
DOCUMENTATION
=============

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

Andrei Paskevich's avatar
Andrei Paskevich committed
18 19
Various examples can be found in the subdirectories theories/
and examples/.
MARCHE Claude's avatar
MARCHE Claude committed
20 21 22 23 24 25 26 27 28 29 30 31 32

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.

Andrei Paskevich's avatar
Andrei Paskevich committed
33 34 35
The files src/util/stdlib.ml{i} are derived from the sources of
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
36 37 38 39

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

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