Rechercher une page de manuel

Chercher une autre page de manuel:

why-obfuscator

Langue: en

Autres versions - même langue

Version: 338031 (ubuntu - 24/10/10)

Section: 1 (Commandes utilisateur)

NAME

why - A multi-language multi-prover verification tool

SYNOPSIS

why [ options ] files

DESCRIPTION

why is a verification tool. It takes annotated programs as input (in ML or C syntax) and outputs verification conditions for several proof assistants (Coq, PVS, HOL Light, Mizar) and decision procedures (haRVey, Simplify).

OPTIONS

-h
Help. Will give you the full list of command line options.

AUTHORS

Jean-Christophe Filliatre <filliatr@lri.fr>

SEE ALSO

Why web site: http://why.lri.fr/

Le problème de la distinction entre nombres premiers et nombres
composés, et celui de la décomposition d'un nombre en produit de
facteurs premiers sont les plus importantes et les plus utiles de toute
l'arithmétique. [...] L'honneur de la science semble exiger qu'on
cultive avec zèle tout progrès dans la solution de ces élégantes et
célèbres questions.
-+- Carl Friedrich Gauss -+-