Package: why-examples (2.23+dfsg-2) [universe]

Links for why-examples

Ubuntu Resources:

Download Source Package why:

Maintainer:

Ubuntu MOTU Developers (Mail Archive)

Please consider filing a bug or asking a question via Launchpad before contacting the maintainer directly.

Original Maintainers (usually from Debian):

Debian OCaml Maintainers (Mail Archive)
Samuel Mimram
Mehdi Dogguy

It should generally not be necessary for users to contact the original maintainer.

External Resources:

Homepage [why.lri.fr]

Similar packages:

Examples of programs certified with Why

Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

This package contains examples of programs verified using Why.

Other Packages Related to why-examples

depends

recommends

suggests

dep: libwhy-coq

Why library for Coq
dep: why

A software verification tool

Download why-examples

Download for all available architectures
Architecture	Package Size	Installed Size	Files
all	180.3 kB	2,160.0 kB	[list of files]