Port details on branch 2022Q3 |
- why3 Deductive program verification platform
- 0.83_2 math
=0 0.83_2Version of this port present on the latest quarterly branch.
- There is no maintainer for this port.
- Any concerns regarding this port should be directed to the FreeBSD Ports mailing list via ports@FreeBSD.org
- Port Added: 2014-06-04 19:22:50
- Last Update: 2021-02-04 09:58:34
- SVN Revision: 564008
- License: LGPL21
- WWW:
- http://why3.lri.fr
- Description:
- 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
wanted.
WWW: http://why3.lri.fr
-
cgit ¦ GitHub ¦ GitHub ¦ GitLab ¦
- Manual pages:
- FreshPorts has no man page information for this port.
- pkg-plist: as obtained via:
make generate-plist - Dependency lines:
-
- Conflicts:
- CONFLICTS_INSTALL:
- Conflicts Matches:
-
There are no Conflicts Matches for this port. This is usually an error.
- No installation instructions:
- This port has been deleted.
- PKGNAME: why3
- Flavors: there is no flavor information for this port.
- distinfo:
- SHA256 (why3-0.83.tar.gz) = cabf67e939e3422e491ef596f1a09ceaf1615642904182097cebde90e42e9ac9
SIZE (why3-0.83.tar.gz) = 5347628
No package information for this port in our database- Sometimes this happens. Not all ports have packages.
- Dependencies
- NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
- Build dependencies:
-
- ocaml-zarith>1.2 : math/ocaml-zarith
- lablgtk2 : x11-toolkits/ocaml-lablgtk2
- ocaml-sqlite3>2 : databases/ocaml-sqlite3
- ocaml-ocamlgraph>1.8 : math/ocaml-ocamlgraph
- camlp5o : devel/ocaml-camlp5
- ocamlc : lang/ocaml
- ocamlfind : devel/ocaml-findlib
- gmake : devel/gmake
- Runtime dependencies:
-
- ocamlc : lang/ocaml
- ocamlfind : devel/ocaml-findlib
- Patch dependencies:
-
- ocamlc : lang/ocaml
-
- There are no ports dependent upon this port
Configuration Options:
- ===> The following configuration options are available for why3-0.83_2:
DOCS=on: Build and/or install documentation
===> Use 'make config' to modify these settings
- Options name:
- N/A
- USES:
- gmake
- FreshPorts was unable to extract/find any pkg message
- Master Sites:
|