Opam Package why3.1.3.3

Package info

opam-namewhy3
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.
authors
  • François Bobot
  • Jean-Christophe Filliâtre
  • Claude Marché
  • Guillaume Melquiond
  • Andrei Paskevich
homepagehttp://why3.lri.fr/
licenseLGPL-2.1-only
deps (9)
revdeps (4)
metas (1)
libraries (1)

Package modules

Package sources

why3

Package files

share/why3/why3session.dtd
share/why3/vim/syntax/why3.vim
share/why3/vim/syntax
share/why3/vim/ftdetect/why3.vim
share/why3/vim/ftdetect
share/why3/vim
share/why3/stdlib/witness.mlw
share/why3/stdlib/tree.mlw
share/why3/stdlib/tptp.mlw
share/why3/stdlib/string.mlw
share/why3/stdlib/stack.mlw
share/why3/stdlib/set.mlw
share/why3/stdlib/seq.mlw
share/why3/stdlib/relations.mlw
share/why3/stdlib/regexp.mlw
share/why3/stdlib/ref.mlw
share/why3/stdlib/real.mlw
share/why3/stdlib/random.mlw
share/why3/stdlib/queue.mlw
share/why3/stdlib/python.mlw
share/why3/stdlib/pqueue.mlw
share/why3/stdlib/pigeon.mlw
share/why3/stdlib/option.mlw
share/why3/stdlib/ocaml.mlw
share/why3/stdlib/number.mlw
share/why3/stdlib/null.mlw
share/why3/stdlib/microc.mlw
share/why3/stdlib/matrix.mlw
share/why3/stdlib/map.mlw
share/why3/stdlib/mach/tagset.mlw
share/why3/stdlib/mach/peano.mlw
share/why3/stdlib/mach/onetime.mlw
share/why3/stdlib/mach/matrix.mlw
share/why3/stdlib/mach/int.mlw
share/why3/stdlib/mach/fxp.mlw
share/why3/stdlib/mach/float.mlw
share/why3/stdlib/mach/c.mlw
share/why3/stdlib/mach/bv.mlw
share/why3/stdlib/mach/array.mlw
share/why3/stdlib/mach
share/why3/stdlib/list.mlw
share/why3/stdlib/io.mlw
share/why3/stdlib/int.mlw
share/why3/stdlib/ieee_float.mlw
share/why3/stdlib/hashtbl.mlw
share/why3/stdlib/graph.mlw
share/why3/stdlib/function.mlw
share/why3/stdlib/for_drivers.mlw
share/why3/stdlib/fmap.mlw
share/why3/stdlib/floating_point.mlw
share/why3/stdlib/exn.mlw
share/why3/stdlib/debug.mlw
share/why3/stdlib/cursor.mlw
share/why3/stdlib/bv.mlw
share/why3/stdlib/bool.mlw
share/why3/stdlib/bintree.mlw
share/why3/stdlib/bag.mlw
share/why3/stdlib/array.mlw
share/why3/stdlib/algebra.mlw
share/why3/stdlib
share/why3/provers-detection-data.conf
share/why3/lang/why3py.lang
share/why3/lang/why3c.lang
share/why3/lang/why3.lang
share/why3/lang
share/why3/drivers/zenon_modulo.drv
share/why3/drivers/zenon.drv
share/why3/drivers/z3_smtv1.drv
share/why3/drivers/z3_bv.gen
share/why3/drivers/z3_471_nobv.drv
share/why3/drivers/z3_471_counterexample.drv
share/why3/drivers/z3_471.drv
share/why3/drivers/z3_440_counterexample.drv
share/why3/drivers/z3_440.drv
share/why3/drivers/z3_432.drv
share/why3/drivers/z3.drv
share/why3/drivers/yices.drv
share/why3/drivers/yices-smt2.drv
share/why3/drivers/why3_tptp.drv
share/why3/drivers/why3_smt.drv
share/why3/drivers/why3.drv
share/why3/drivers/verit.drv
share/why3/drivers/vampire.drv
share/why3/drivers/vampire-smt.drv
share/why3/drivers/tptp.gen
share/why3/drivers/tptp-tff1.drv
share/why3/drivers/tptp-tff0.drv
share/why3/drivers/spass_types.drv
share/why3/drivers/spass.drv
share/why3/drivers/smtlib-strings.gen
share/why3/drivers/smt-libv2.gen
share/why3/drivers/smt-libv2.drv
share/why3/drivers/smt-libv2-gnatprove.gen
share/why3/drivers/smt-libv2-floats.gen
share/why3/drivers/smt-libv2-floats-int_via_real.gen
share/why3/drivers/smt-libv2-floats-int_via_bv.gen
share/why3/drivers/smt-libv2-floats-gnatprove.gen
share/why3/drivers/smt-libv2-bv.gen
share/why3/drivers/smt-libv2-bv-realization.gen
share/why3/drivers/simplify.drv
share/why3/drivers/safeprover.drv
share/why3/drivers/pvs.drv
share/why3/drivers/pvs-realize.drv
share/why3/drivers/pvs-realizations.aux
share/why3/drivers/pvs-common.gen
share/why3/drivers/psyche.drv
share/why3/drivers/princess.drv
share/why3/drivers/polypaver.drv
share/why3/drivers/ocaml64.drv
share/why3/drivers/ocaml-unsafe-int.drv
share/why3/drivers/no-bv.gen
share/why3/drivers/metitarski.drv
share/why3/drivers/metis.drv
share/why3/drivers/mathsat.drv
share/why3/drivers/mathematica.drv
share/why3/drivers/isabelle2019.drv
share/why3/drivers/isabelle2019-realize.drv
share/why3/drivers/isabelle2018.drv
share/why3/drivers/isabelle2018-realize.drv
share/why3/drivers/isabelle-realizations.aux
share/why3/drivers/isabelle-common.gen
share/why3/drivers/iprover.drv
share/why3/drivers/gappa.drv
share/why3/drivers/eprover.drv
share/why3/drivers/discrimination.gen
share/why3/drivers/cvc4_bv.gen
share/why3/drivers/cvc4_17_strings_counterexample.drv
share/why3/drivers/cvc4_17_strings.drv
share/why3/drivers/cvc4_17_counterexample.drv
share/why3/drivers/cvc4_17.drv
share/why3/drivers/cvc4_16_counterexample.drv
share/why3/drivers/cvc4_16.gen
share/why3/drivers/cvc4_16.drv
share/why3/drivers/cvc4_15_counterexample.drv
share/why3/drivers/cvc4_15.drv
share/why3/drivers/cvc4_14.drv
share/why3/drivers/cvc4.drv
share/why3/drivers/cvc4-realize.drv
share/why3/drivers/cvc3.drv
share/why3/drivers/coq.drv
share/why3/drivers/coq-ssreflect.drv
share/why3/drivers/coq-realize.drv
share/why3/drivers/coq-realizations.aux
share/why3/drivers/coq-common.gen
share/why3/drivers/cakeml.drv
share/why3/drivers/c.drv
share/why3/drivers/beagle.drv
share/why3/drivers/alt_ergo_smt2.drv
share/why3/drivers/alt_ergo_model.drv
share/why3/drivers/alt_ergo_fp.drv
share/why3/drivers/alt_ergo_common.drv
share/why3/drivers/alt_ergo_2_2_0.drv
share/why3/drivers/alt_ergo.drv
share/why3/drivers
share/why3/Makefile.config
share/why3/LICENSE
share/why3
share/emacs/site-lisp/why3.elc
share/emacs/site-lisp/why3.el
lib/why3/why3server
lib/why3/why3cpulimit
lib/why3/why3.cmxs
lib/why3/why3.cmxa
lib/why3/why3.cmx
lib/why3/why3.cmi
lib/why3/why3.cma
lib/why3/why3.a
lib/why3/why3-call-pvs
lib/why3/plugins/tptp.cmxs
lib/why3/plugins/tptp.cmo
lib/why3/plugins/python.cmxs
lib/why3/plugins/python.cmo
lib/why3/plugins/microc.cmxs
lib/why3/plugins/microc.cmo
lib/why3/plugins/genequlin.cmxs
lib/why3/plugins/genequlin.cmo
lib/why3/plugins/dimacs.cmxs
lib/why3/plugins/dimacs.cmo
lib/why3/plugins
lib/why3/commands/why3webserver
lib/why3/commands/why3wc
lib/why3/commands/why3shell
lib/why3/commands/why3session
lib/why3/commands/why3replay
lib/why3/commands/why3realize
lib/why3/commands/why3prove
lib/why3/commands/why3pp
lib/why3/commands/why3extract
lib/why3/commands/why3execute
lib/why3/commands/why3doc
lib/why3/commands/why3config
lib/why3/commands
lib/why3/META
lib/why3
bin/why3