why3 - Deductive program verification platform

Property Value
Distribution FreeBSD 10
Repository FreeBSD Ports Latest amd64
Package name why3
Package version 0.83
Package release 2
Package architecture amd64
Package type txz
Installed size 75.24 MB
Download size 13.40 MB
Official Mirror pkg.freebsd.org
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
Categories: math
Maintainer: ports@FreeBSD.org
- 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
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-b19_14.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_7.txz Wiimms ISO Tools
wikicalc-1.0.txz Open Source Wiki-Spreadsheet
wildfly10-10.1.0_1.txz Replacement for JBoss Application Server
wildfly11-11.0.0.txz Replacement for JBoss Application Server
wildfly12-12.0.0.txz Replacement for JBoss Application Server
wildfly13-13.0.0.txz Replacement for JBoss Application Server
wildfly14-14.0.1.txz Replacement for JBoss Application Server
wildfly90-9.0.2_1.txz Replacement for JBoss Application Server
wildmidi-0.4.2.txz Simple software midi player and core softsynth library
wimlib-1.12.0.txz Manipulate Windows Imaging (WIM) archives