Commit c82a4f94 authored by Andrei Paskevich's avatar Andrei Paskevich

Why3 presentation in README and the foreword of the manual

parent ae198377
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.
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.
PROJECT HOME
============
http://why3.lri.fr
https://gforge.inria.fr/projects/why3
DOCUMENTATION
......@@ -30,7 +38,7 @@ COPYRIGHT
This program is distributed under the GNU LGPL 2.1. See the enclosed
file LICENSE.
The files src/util/stdlib.ml{i} are derived from the sources of
The files src/util/extmap.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).
......
......@@ -145,10 +145,23 @@ $^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
\chapter*{Foreword}
This is the manual for the Why platform version 3, or \why for
short. \why is a complete reimplementation~\cite{boogie11why3} of the former Why
platform~\cite{filliatre07cav} for program
verification. Among the new features are: numerous
%This is the manual for the Why platform version 3, or \why for
%short.
\why 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. \why 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.
\why is a complete reimplementation %~\cite{boogie11why3}
of the former Why platform~\cite{filliatre07cav}.
%for program verification.
Among the new features are: numerous
extensions to the input language, a new architecture for calling
external provers, and a well-designed API, allowing to use \why as a
software library. An important emphasis is put on modularity and
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment