Opam Package why3-coq.1.3.3

Package info

opam-namewhy3-coq
opam-version1.3.3
synopsisWhy3 environment for deductive program verification
description Why3 provides a rich 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. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted. This package provides the Coq realizations of Why3 theories.
authors
  • François Bobot
  • Jean-Christophe Filliâtre
  • Claude Marché
  • Guillaume Melquiond
  • Andrei Paskevich
homepagehttp://why3.lri.fr/
licenseLGPL-2.1-only
deps (5)
revdeps(0)
metas(0)
libraries(0)

Package modules

Package sources

why3-coq

Package files

lib/why3/coq/version
lib/why3/coq/set/SetImpInt.vo
lib/why3/coq/set/SetImp.vo
lib/why3/coq/set/SetAppInt.vo
lib/why3/coq/set/SetApp.vo
lib/why3/coq/set/Set.vo
lib/why3/coq/set/FsetSum.vo
lib/why3/coq/set/FsetInt.vo
lib/why3/coq/set/FsetInduction.vo
lib/why3/coq/set/Fset.vo
lib/why3/coq/set/Cardinal.vo
lib/why3/coq/set
lib/why3/coq/real/Trigonometry.vo
lib/why3/coq/real/Square.vo
lib/why3/coq/real/RealInfix.vo
lib/why3/coq/real/Real.vo
lib/why3/coq/real/PowerReal.vo
lib/why3/coq/real/PowerInt.vo
lib/why3/coq/real/MinMax.vo
lib/why3/coq/real/FromInt.vo
lib/why3/coq/real/ExpLog.vo
lib/why3/coq/real/Abs.vo
lib/why3/coq/real
lib/why3/coq/option/Option.vo
lib/why3/coq/option
lib/why3/coq/number/Prime.vo
lib/why3/coq/number/Parity.vo
lib/why3/coq/number/Gcd.vo
lib/why3/coq/number/Divisibility.vo
lib/why3/coq/number/Coprime.vo
lib/why3/coq/number
lib/why3/coq/map/Occ.vo
lib/why3/coq/map/MapPermut.vo
lib/why3/coq/map/MapInjection.vo
lib/why3/coq/map/Map.vo
lib/why3/coq/map/Const.vo
lib/why3/coq/map
lib/why3/coq/list/Reverse.vo
lib/why3/coq/list/RevAppend.vo
lib/why3/coq/list/Permut.vo
lib/why3/coq/list/NumOcc.vo
lib/why3/coq/list/NthNoOpt.vo
lib/why3/coq/list/NthLengthAppend.vo
lib/why3/coq/list/NthLength.vo
lib/why3/coq/list/NthHdTl.vo
lib/why3/coq/list/Nth.vo
lib/why3/coq/list/Mem.vo
lib/why3/coq/list/List.vo
lib/why3/coq/list/Length.vo
lib/why3/coq/list/HdTlNoOpt.vo
lib/why3/coq/list/HdTl.vo
lib/why3/coq/list/Distinct.vo
lib/why3/coq/list/Combine.vo
lib/why3/coq/list/Append.vo
lib/why3/coq/list
lib/why3/coq/int/Power.vo
lib/why3/coq/int/NumOf.vo
lib/why3/coq/int/MinMax.vo
lib/why3/coq/int/Int.vo
lib/why3/coq/int/Exponentiation.vo
lib/why3/coq/int/EuclideanDivision.vo
lib/why3/coq/int/Div2.vo
lib/why3/coq/int/ComputerDivision.vo
lib/why3/coq/int/Abs.vo
lib/why3/coq/int
lib/why3/coq/for_drivers/ComputerOfEuclideanDivision.vo
lib/why3/coq/for_drivers
lib/why3/coq/bv/Pow2int.vo
lib/why3/coq/bv/BV_Gen.vo
lib/why3/coq/bv
lib/why3/coq/bool/Bool.vo
lib/why3/coq/bool
lib/why3/coq/HighOrd.vo
lib/why3/coq/BuiltIn.vo
lib/why3/coq