why3 - Deductive program verification platform

Property Value
Distribution FreeBSD 12
Repository FreeBSD Ports Latest amd64
Package filename why3-0.83_2.txz
Package name why3
Package version 0.83
Package release 2
Package architecture amd64
Package type txz
Category math
Homepage http://why3.lri.fr
License LGPL21
Maintainer ports@FreeBSD.org
Download size 13.12 MB
Installed size 74.53 MB
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.
Why3 is a complete reimplementation of the former Why platform. 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 Why3 as a software library. An important emphasis is put
on modularity and genericity, giving the end user a possibility to easily
reuse Why3 formalizations or to add support for a new external prover if
WWW: http://why3.lri.fr
- DOCS: on
===>   NOTICE:
The why3 port currently does not have a maintainer. As a result, it is
more likely to have unresolved issues, not be up-to-date, or even be removed in
the future. To volunteer to maintain this port, please create an issue at:
More information about port maintainership is available at:


Package Version Architecture Repository
why3-0.83_2.txz 0.83 i386 FreeBSD Ports Quarterly
why3-0.83_2.txz 0.83 amd64 FreeBSD Ports Quarterly
why3-0.83_2.txz 0.83 i386 FreeBSD Ports Latest
why3 - - -


Name Value
libatk-1.0.so.0 -
libcairo.so.2 -
libfontconfig.so.1 -
libfreetype.so.6 -
libgdk-x11-2.0.so.0 -
libgdk_pixbuf-2.0.so.0 -
libgio-2.0.so.0 -
libglib-2.0.so.0 -
libgobject-2.0.so.0 -
libgtk-x11-2.0.so.0 -
libgtksourceview-2.0.so.0 -
libintl.so.8 -
libpango-1.0.so.0 -
libpangocairo-1.0.so.0 -
libpangoft2-1.0.so.0 -
libsqlite3.so.0 -
ocaml = 4.02.3
ocaml-findlib = 1.7.1


Type URL
Mirror pkg.freebsd.org
Binary Package why3-0.83_2.txz
Source Package math/why3

Install Howto

Install why3 txz package:

# pkg install why3

See Also

Package Description
whysynth-20120903_4.txz Versatile softsynth implemented as a DSSI plugin
widelands-b20_3.txz Realtime strategy game inspired by Settlers II
widentd-1.04.txz RFC1413 auth/identd daemon providing a fixed fake reply
wifimgr-1.12.txz WiFi Networks Manager
wiggle-1.1.txz Apply rejected patches and perform word-wise diffs
wiimms-2.23.a_9.txz Wiimms ISO Tools
wikicalc-1.0.txz Open Source Wiki-Spreadsheet
wildfly10-10.1.0_2.txz Replacement for JBoss Application Server
wildfly11-11.0.0_1.txz Replacement for JBoss Application Server
wildfly12-12.0.0_1.txz Replacement for JBoss Application Server
wildfly13-13.0.0_1.txz Replacement for JBoss Application Server
wildfly14-14.0.1.txz Replacement for JBoss Application Server
wildfly15-15.0.1.txz Replacement for JBoss Application Server
wildfly16-16.0.0.txz Replacement for JBoss Application Server
wildfly90-9.0.2_2.txz Replacement for JBoss Application Server