Poster of Linux kernelThe best gift for a Linux geek
why

why

Section: User Commands (1) Updated: March, 2002
Local index Up

 

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/


 

Index

NAME
SYNOPSIS
DESCRIPTION
OPTIONS
AUTHORS
SEE ALSO

This document was created by man2html, using the manual pages.
Time: 21:26:58 GMT, April 16, 2011