why3
Deductive program verification
Why3 provides a 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.
- Versions: 1.7.2
- Website: https://why3.lri.fr
- Licenses: LGPL 2.1
- Package source: gnu/packages/maths.scm
- Builds: See build status
- Issues: See known issues
Installation
Install the latest version of why3 as follows:
guix install why3
Or install a particular version:
guix install why3@1.7.2
You can also install packages in augmented, pure or containerized environments for development or simply to try them out without polluting your user profile. See the guix shell documentation for more information.
Badge code
You can use the following badge to inform users of why3 about the latest version available in Guix.
Example HTML:
<a href='https://packages.guix.gnu.org/packages/why3'><img src='https://packages.guix.gnu.org/packages/why3/badges/latest-version.svg' alt='Version in GNU Guix'></a>
Example Markdown:
[](https://packages.guix.gnu.org/packages/why3)
Example Org:
[[https://packages.guix.gnu.org/packages/why3][https://packages.guix.gnu.org/packages/why3/badges/latest-version.svg]]