» Ubuntu » Balíky » lucid (10.04LTS) » doc » why-examples
lucid  ] [  precise  ] [  utopic  ] [  vivid  ]
[ Zdroj: why  ]

Balík: why-examples (2.23+dfsg-2) [universe]

Odkazy pre why-examples

Screenshot

Zdroje Ubuntu:

Stiahnuť zdrojový balík why:

Správca:

Please consider filing a bug or asking a question via Launchpad before contacting the maintainer directly.

Original Maintainers (usually from Debian):

  • Debian OCaml Maintainers (Konferencia)
  • Samuel Mimram
  • Mehdi Dogguy

It should generally not be necessary for users to contact the original maintainer.

Externé zdroje:

Podobné balíky:

Examples of programs certified with Why

Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.

This package contains examples of programs verified using Why.

Ostatné balíky súvisiace s balíkom why-examples

  • závisí
  • odporúča
  • navrhuje
  • enhances
  • dep: libwhy-coq
    Why library for Coq
  • dep: why
    A software verification tool

Stiahnuť why-examples

Stiahnuť pre všetky dostupné architektúry
Architektúra Veľkosť balíka Nainštalovaná veľkosť Súbory
all 180.3 kB2,160.0 kB [zoznam súborov]