package alt-ergo-plugin-ab-why3

  1. Overview
  2. No Docs
An experimental Why3 frontend for Alt-Ergo

Install

alt-ergo.ocamlpro.com Edit opam file

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. A
    Alt-Ergo developers

Sources

alt-ergo-2.5.1.tbz
sha256=9cf8d69a0e457a939b86aba2a18c6154faba51d387b42a361ece55d329dd601d
sha512=09694d18496ba1938daaa7b4e28e6b3d6811687dd3aaede17917f20511be9d8328394fac021af683d4c0217d4b030da9a60a5b9c14d968f1948735ea7ec52543

Description

An experimental front-end that parses a subset of Why3's logic. More precisely, this front-end targets proof obligations generated by the Atelier-B framework in Why3 format. It should be used with a prelude defining the B Set theory.

Published: 15 Sep 2023

Dependencies (4)

  1. alt-ergo-parsers = version
  2. alt-ergo-lib = version
  3. alt-ergo = version
  4. dune >= "3.0"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None