Why3 API documentation

Args_wrapper

Pre-processing of transformations with arguments, including parsing and typing in the context of a task.

BigInt

Wrapper for big nums, implemented either with OCaml's Nums or ZArith

Call_provers

Call provers and parse their outputs

Check_ce

Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking

Coercion

Support for coercions in the logic language

Controller_itp

Controller to run provers and transformations asynchronously on goals of a session

Debug

Debug flag handling

Decl

Logic Declarations

Driver

Managing the drivers for external provers

Env

Why3 Environments

Expr

WhyML program expressions

Exthtbl

Association tables over hashable types

Extmap

Association tables over ordered types

Extset

Sets over ordered types

Getopt

Parsing of command-line options

Ident

Identifiers

Itp_communication

Communication protocol for the ITP server

Itp_server

Server for a client/server communication with an external graphical interface

Ity

Types in WhyML programs

Lists

Combinators on list type

Loc

Source locations

Mlmpfr_wrapper

Wrapper module for computation on extended floating-point numbers

Mlw_printer

Pretty printing of Why3 parse trees as WhyML source code

Model_parser

Model

Number

General functions for representations of numeric values

Opt

Combinators on option type

Pdecl

WhyML program declarations

Pinterp

WhyML Program Interpreter

Pinterp_core

WhyML program interpreter: basic definitions

Pmodule

WhyML program modules

Pp

Helpers for formatted pretty-printing

Pretty
Printer

Task printing

Ptree

Parse trees

Ptree_helpers

Helpers for constructing program with the parse tree API

Rac

Runtime Assertion Checkers for WhyML programs

Rc

Configuration file management

Session_itp

Proof sessions

Strings

Utility Functions on Character Strings

Task

Proof Tasks, Cloning and Meta History

Term

Terms and Formulas

Theory

Theories and Namespaces

Trans

Task transformations

Ty

Types

Typing

Typing parse trees

Util

Various Utility Functions

Vc

WhyML VC generators

Weakhtbl

Hashtables with weak key used for memoization

Whyconf

Managing the configuration of Why3

Wstdlib

Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types