_            _    _        _         _
      /\ \         /\ \ /\ \     /\_\      / /\
      \_\ \       /  \ \\ \ \   / / /     / /  \
      /\__ \     / /\ \ \\ \ \_/ / /     / / /\ \__
     / /_ \ \   / / /\ \ \\ \___/ /     / / /\ \___\
    / / /\ \ \ / / /  \ \_\\ \ \_/      \ \ \ \/___/
   / / /  \/_// / /   / / / \ \ \        \ \ \
  / / /      / / /   / / /   \ \ \   _    \ \ \
 / / /      / / /___/ / /     \ \ \ /_/\__/ / /
/_/ /      / / /____\/ /       \ \_\\ \/___/ /
\_\/       \/_________/         \/_/ \_____\/
why3 1.7.2
Dependencies: coq-flocq@4.1.4 emacs-minimal@30.2 zlib@1.3.1
Propagated dependencies: camlzip@1.11 lablgtk@3.1.3 ocaml-graph@2.0.0 ocaml-lablgtk3-sourceview3@3.1.3 ocaml-menhir@20220210 ocaml-ppx-deriving@5.2.1 ocaml-ppx-sexp-conv@0.15.1 ocaml-num@1.4 ocaml-re@1.10.4 ocaml-sexplib@0.16.0 ocaml-zarith@1.12
Channel: guix
Location: gnu/packages/maths.scm (gnu packages maths)
Home page: https://why3.lri.fr
Licenses: LGPL 2.1
Synopsis: Deductive program verification
Description:

Why3 provides a 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.

Total results: 1