Why3 Standard Library

• algebra : Basic Algebra Theories
• array : Arrays
• bag : Multisets (aka bags)
• bintree : Polymorphic binary trees with elements at nodes
• bool : Booleans
• bv : Bit Vectors
• cursor : Cursors
• exn : General-purpose exceptions
• floating_point : Formalization of Floating-Point Arithmetic
• fmap : Finite Domain Maps
• function : Injections, surjections and bijections
• graph : Graph theory
• hashtbl : Hash tables
• ieee_float : Formalization of Floating-Point Arithmetic
• int : Theory of integers
• io : Basic I/O Functions
• list : Polymorphic Lists
• map : Theory of maps
• matrix : Matrices
• number : Number theory
• ocaml : General functions related to OCaml extraction
• option : Option type
• pigeon : Pigeon hole principle
• pqueue : Priority queues
• queue : Polymorphic mutable queues
• random : Pseudo-random generators
• real : Theory of reals
• ref : References
• regexp : Theory of regular expressions
• relations : Relations
• seq : Sequences
• set : Set theories
• stack : Stacks
• string : Theory of strings
• tree : Polymorphic n-ary trees
• ufloat : Unbounded floating-point numbers
• witness : Witnesses of existential proofs
• mach.array : Arrays with bounded-size integers
• mach.bv : Program functions on bitvectors with preconditions
• mach.c : A lightweight memory model dedicated to extraction to C code
• mach.float : Floating-Point Computations with overflow check
• mach.fxp : Fixed-point computations
• mach.int : Machine Arithmetic
• mach.matrix : Matrices with bounded-size integers
• mach.onetime : One-time integers
• mach.peano : Peano arithmetic
• mach.tagset : Tag Sets
• mach.java.lang : Modules that mimics some classes from JDK package java.lang
• mach.java.util : Modules that mimics some classes from JDK package java.util