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

.