why3.lri.fr

Why3 Overview 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 automate...

Why3 theory, one can use a proof assistant to make a realization of this theory, that is to provide definitions for some of its uninterpreted symbols and proofs for some of its axioms. This way, one ...

Integers and the basic operators theory Int constant zero : int = 0 constant one : int = 1 predicate (< ) int int predicate (> ) (x y : int) = y < x predicate (<=) (x y : int) = x < y \...

6.1  The why3config command-line tool Why3 must be configured to access external provers. Typically, this is done by running the command line tool why3config. This must be redone each time a new pro...