why 2.34-4ubuntu5 source package in Ubuntu

Changelog

why (2.34-4ubuntu5) yakkety; urgency=medium

  * No-change rebuild against frama-c 20151002+magnesium+dfsg-1build2

 -- Steve Langasek <email address hidden>  Sun, 10 Jul 2016 13:41:00 -0700

Upload details

Uploaded by:
Steve Langasek on 2016-07-10
Uploaded to:
Yakkety
Original maintainer:
Ubuntu Developers
Architectures:
any all
Section:
math
Urgency:
Medium Urgency

See full publishing history Publishing

Series Pocket Published Component Section
Zesty release on 2016-10-18 universe math
Yakkety release on 2016-07-11 universe math

Downloads

File Size SHA-256 Checksum
why_2.34.orig.tar.gz 3.6 MiB 76f3af8cf3857424852ca76eb87c99ff6089aadc3271da6b829ca84529f9c733
why_2.34-4ubuntu5.debian.tar.xz 11.2 KiB 877960ee14253021429a9c9b47fba6011989de97ab3c15aff7c5c46f288c05d8
why_2.34-4ubuntu5.dsc 2.3 KiB 6ab93a3dff02d24f60ad73422f26d8a2ffee38ed62484de80f4b7ec5669bd65e

Available diffs

View changes file

Binary packages built by this source

why: Software verification tool for C and Java

 This package contains Krakatoa and Jessie, two front-ends of the Why3
 platform for deductive program verification. Krakatoa deals with Java
 programs annotated in a variant of the The Java Modeling
 Language. Jessie deals with C programs annotated in the ANSI/ISO C
 Specification Language (ACSL).

why-dbgsym: debug symbols for package 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.

why-examples: 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.