diff options
Diffstat (limited to 'devel/why/DETAILS')
| -rwxr-xr-x | devel/why/DETAILS | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/devel/why/DETAILS b/devel/why/DETAILS new file mode 100755 index 0000000000..a9db03d016 --- /dev/null +++ b/devel/why/DETAILS @@ -0,0 +1,26 @@ + SPELL=why + VERSION=2.33 + SOURCE="${SPELL}-${VERSION}.tar.gz" + SOURCE_URL[0]=http://${SPELL}.lri.fr/download/${SOURCE} + SOURCE_HASH=sha512:aef4fc09b23600bc76203b1b276afcde0035e1186f899c007c5fe183345dc4b93bddf3f27abd1a3c0830cc3ebf127b6eaba20f54b22deeedd5d2723a012f9746 +SOURCE_DIRECTORY="${BUILD_DIRECTORY}/${SPELL}-${VERSION}" + WEB_SITE="http://why.lri.fr" + LICENSE[0]=GPL + ENTERED=20120305 + SHORT="a software verification platform" +cat << EOF +Why is a software verification platform. + +This platform contains several tools: + +* a general-purpose verification condition generator (VCG), Why, which is used + as a back-end by other verification tools (see below) but which can also + be used directly to verify programs (see for instance these examples) ; +* a tool Krakatoa for the verification of Java programs; * a tool Caduceus +for the verification of C programs; note that Caduceus is + somewhat obsolete now and users should turn to Frama-C instead. + +One of the main features of Why is to be integrated with many existing provers +(proof assistants such as Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar +and decision procedures such as Simplify, Alt-Ergo, Yices, Z3, CVC3, etc.). +EOF |