why-examples_2.30+dfsg-5_all.deb


Advertisement

Description

why-examples - Examples of programs certified with Why

Property Value
Distribution Debian 7 (Wheezy)
Repository Debian Main amd64
Package name why-examples
Package version 2.30+dfsg
Package release 5
Package architecture all
Package type deb
Installed size 1.60 KB
Download size 189.86 KB
Official Mirror ftp.br.debian.org
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.

Alternatives

Package Version Architecture Repository
why-examples_2.30+dfsg-5_all.deb 2.30+dfsg all Debian Main
why-examples - - -

Requires

Name Value
libwhy-coq -
why -

Download

Type URL
Binary Package why-examples_2.30+dfsg-5_all.deb
Source Package why

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install why-examples deb package:
    # sudo apt-get install why-examples

Files

Path
/usr/share/doc/why-examples/changelog.Debian.gz
/usr/share/doc/why-examples/changelog.gz
/usr/share/doc/why-examples/copyright
/usr/share/doc/why/examples/Makefile
/usr/share/doc/why/examples/Makefile.common
/usr/share/doc/why/examples-c/Makefile
/usr/share/doc/why/examples-c/float/Malcolm.c
/usr/share/doc/why/examples-c/float/Sterbenz.c
/usr/share/doc/why/examples-c/float/Sterbenz2.c
/usr/share/doc/why/examples-c/float/coq/Malcolm_spec_why.v
/usr/share/doc/why/examples-c/float/coq/Malcolm_why.v
/usr/share/doc/why/examples-c/float/coq/Sterbenz2_why.v
/usr/share/doc/why/examples-c/float/coq/Sterbenz_why.v
/usr/share/doc/why/examples-c/g4/Makefile
/usr/share/doc/why/examples-c/g4/g4.c
/usr/share/doc/why/examples-c/g4/coq/G4.v
/usr/share/doc/why/examples-c/g4/coq/G4z.v
/usr/share/doc/why/examples-c/g4/coq/Lex3.v
/usr/share/doc/why/examples-c/g4/coq/g4_why.v
/usr/share/doc/why/examples-c/g4/coq/nat_of_Z.v
/usr/share/doc/why/examples-c/linked-lists/Makefile
/usr/share/doc/why/examples-c/linked-lists/has_cycle.c
/usr/share/doc/why/examples-c/linked-lists/list.h
/usr/share/doc/why/examples-c/linked-lists/reverse.c
/usr/share/doc/why/examples-c/linked-lists/search.c
/usr/share/doc/why/examples-c/linked-lists/swap.c
/usr/share/doc/why/examples-c/linked-lists/coq/has_cycle_why.v
/usr/share/doc/why/examples-c/linked-lists/coq/reverse_spec_why.v
/usr/share/doc/why/examples-c/linked-lists/coq/reverse_why.v
/usr/share/doc/why/examples-c/linked-lists/coq/search_why.v
/usr/share/doc/why/examples-c/linked-lists/coq/swap_spec_why.v
/usr/share/doc/why/examples-c/linked-lists/coq/swap_why.v
/usr/share/doc/why/examples-c/puf/Makefile
/usr/share/doc/why/examples-c/puf/parray.c
/usr/share/doc/why/examples-c/puf/parray_frama_c.c
/usr/share/doc/why/examples-c/puf/puf.c
/usr/share/doc/why/examples-c/schorr-waite/Makefile
/usr/share/doc/why/examples-c/schorr-waite/schorr_waite.c
/usr/share/doc/why/examples-c/schorr-waite/coq/BinTree.v
/usr/share/doc/why/examples-c/schorr-waite/coq/GenericLists.v
/usr/share/doc/why/examples-c/schorr-waite/coq/caduceus_spec_why.v
/usr/share/doc/why/examples-c/schorr-waite/coq/schorr_waite_spec_why.v
/usr/share/doc/why/examples-c/schorr-waite/coq/schorr_waite_why.v
/usr/share/doc/why/examples-c/sorting/Makefile
/usr/share/doc/why/examples-c/sorting/quicksort.c
/usr/share/doc/why/examples-c/sorting/selection.c
/usr/share/doc/why/examples-c/sorting/coq/MSet.v
/usr/share/doc/why/examples-c/sorting/coq/selection_spec_why.v
/usr/share/doc/why/examples-c/sorting/coq/selection_why.v
/usr/share/doc/why/examples-c/trees/Makefile
/usr/share/doc/why/examples-c/trees/search.c
/usr/share/doc/why/examples-c/trees/tree.h
/usr/share/doc/why/examples-c/tutorial/Makefile
/usr/share/doc/why/examples-c/tutorial/abs.c
/usr/share/doc/why/examples-c/tutorial/average.c
/usr/share/doc/why/examples-c/tutorial/binary_search.c
/usr/share/doc/why/examples-c/tutorial/flag.c
/usr/share/doc/why/examples-c/tutorial/max.c
/usr/share/doc/why/examples-c/tutorial/modulo.c
/usr/share/doc/why/examples-c/tutorial/purse.c
/usr/share/doc/why/examples-c/tutorial/search.c
/usr/share/doc/why/examples-c/tutorial/swap.c
/usr/share/doc/why/examples-c/tutorial/coq/abs_spec_why.v
/usr/share/doc/why/examples-c/tutorial/coq/abs_why.v
/usr/share/doc/why/examples-c/tutorial/coq/average_why.v
/usr/share/doc/why/examples-c/tutorial/coq/binary_search_why.v
/usr/share/doc/why/examples-c/tutorial/coq/flag_why.v
/usr/share/doc/why/examples-c/tutorial/coq/max_spec_why.v
/usr/share/doc/why/examples-c/tutorial/coq/max_why.v
/usr/share/doc/why/examples-c/tutorial/coq/modulo_why.v
/usr/share/doc/why/examples-c/tutorial/coq/purse_spec_why.v
/usr/share/doc/why/examples-c/tutorial/coq/purse_why.v
/usr/share/doc/why/examples-c/tutorial/coq/search_spec_why.v
/usr/share/doc/why/examples-c/tutorial/coq/search_why.v
/usr/share/doc/why/examples-c/tutorial/coq/swap_spec_why.v
/usr/share/doc/why/examples-c/tutorial/coq/swap_why.v
/usr/share/doc/why/examples-c/ukkonen/main.c
/usr/share/doc/why/examples-c/ukkonen/ukkonen.c.gz
/usr/share/doc/why/examples/algo-63-64-65/.depend
/usr/share/doc/why/examples/algo-63-64-65/Makefile
/usr/share/doc/why/examples/algo-63-64-65/algo63.mlw
/usr/share/doc/why/examples/algo-63-64-65/algo64.mlw
/usr/share/doc/why/examples/algo-63-64-65/algo64_why.v
/usr/share/doc/why/examples/algo-63-64-65/algo65.mlw
/usr/share/doc/why/examples/binary-search/.depend
/usr/share/doc/why/examples/binary-search/Makefile
/usr/share/doc/why/examples/binary-search/bsearch.mlw
/usr/share/doc/why/examples/binary-search/bsearch_why.sx
/usr/share/doc/why/examples/binary-search/bsearch_why.v
/usr/share/doc/why/examples/bresenham/.depend
/usr/share/doc/why/examples/bresenham/Makefile
/usr/share/doc/why/examples/bresenham/bresenham.mlw
/usr/share/doc/why/examples/bresenham/bresenham_coq.mlw
/usr/share/doc/why/examples/bresenham/bresenham_coq_why.v
/usr/share/doc/why/examples/bresenham/bresenham_inv.mlw
/usr/share/doc/why/examples/bresenham/bresenham_why.v
/usr/share/doc/why/examples/bresenham/zaux.v
/usr/share/doc/why/examples/dijkstra/.depend
/usr/share/doc/why/examples/dijkstra/Makefile
/usr/share/doc/why/examples/dijkstra/dijkstra.why
/usr/share/doc/why/examples/dijkstra/dijkstra_why.v
/usr/share/doc/why/examples/edit-distance/.depend
/usr/share/doc/why/examples/edit-distance/Makefile
/usr/share/doc/why/examples/edit-distance/distance.mlw
/usr/share/doc/why/examples/edit-distance/distance_why.sx
/usr/share/doc/why/examples/edit-distance/distance_why.v
/usr/share/doc/why/examples/edit-distance/words.v
/usr/share/doc/why/examples/find/.depend
/usr/share/doc/why/examples/find/Makefile
/usr/share/doc/why/examples/find/find.mlw
/usr/share/doc/why/examples/find/find_lemmas.v
/usr/share/doc/why/examples/find/find_proofs.v
/usr/share/doc/why/examples/find/find_spec.v
/usr/share/doc/why/examples/find/find_why.v
/usr/share/doc/why/examples/heapsort/.depend
/usr/share/doc/why/examples/heapsort/Inftree.v
/usr/share/doc/why/examples/heapsort/Makefile
/usr/share/doc/why/examples/heapsort/downheap.mlw
/usr/share/doc/why/examples/heapsort/downheap_why.v
/usr/share/doc/why/examples/heapsort/heap.v
/usr/share/doc/why/examples/heapsort/heapsort.mlw
/usr/share/doc/why/examples/heapsort/heapsort_why.v
/usr/share/doc/why/examples/heapsort/swap.mlw
/usr/share/doc/why/examples/heapsort/swap_why.v
/usr/share/doc/why/examples/kmp/.depend
/usr/share/doc/why/examples/kmp/Lex.v
/usr/share/doc/why/examples/kmp/Makefile
/usr/share/doc/why/examples/kmp/Match.v
/usr/share/doc/why/examples/kmp/Next.v
/usr/share/doc/why/examples/kmp/kmp.mlw
/usr/share/doc/why/examples/kmp/kmp_why.v
/usr/share/doc/why/examples/linked-lists/.depend
/usr/share/doc/why/examples/linked-lists/LinkedLists.v
/usr/share/doc/why/examples/linked-lists/Makefile
/usr/share/doc/why/examples/linked-lists/length.mlw
/usr/share/doc/why/examples/linked-lists/length_why.v
/usr/share/doc/why/examples/linked-lists/rev.mlw
/usr/share/doc/why/examples/linked-lists/rev_why.v
/usr/share/doc/why/examples/linked-lists/reverse.why
/usr/share/doc/why/examples/maximumsort/.depend
/usr/share/doc/why/examples/maximumsort/Makefile
/usr/share/doc/why/examples/maximumsort/maximumsort.mlw
/usr/share/doc/why/examples/maximumsort/maximumsort_why.sx
/usr/share/doc/why/examples/maximumsort/maximumsort_why.v
/usr/share/doc/why/examples/mergesort/.depend
/usr/share/doc/why/examples/mergesort/Makefile
/usr/share/doc/why/examples/mergesort/mergesort.mlw
/usr/share/doc/why/examples/mergesort/mergesort.why
/usr/share/doc/why/examples/misc/.depend
/usr/share/doc/why/examples/misc/Makefile
/usr/share/doc/why/examples/misc/arith.mlw
/usr/share/doc/why/examples/misc/arith_why.sx
/usr/share/doc/why/examples/misc/arith_why.v
/usr/share/doc/why/examples/misc/copy_why.sx
/usr/share/doc/why/examples/misc/copy_why.v
/usr/share/doc/why/examples/misc/csearch_why.sx
/usr/share/doc/why/examples/misc/csearch_why.v
/usr/share/doc/why/examples/misc/fib.mlw
/usr/share/doc/why/examples/misc/fib_why.sx
/usr/share/doc/why/examples/misc/fib_why.v
/usr/share/doc/why/examples/misc/flag.mlw
/usr/share/doc/why/examples/misc/flag_ax.mlw
/usr/share/doc/why/examples/misc/flag_ax_why.sx
/usr/share/doc/why/examples/misc/flag_ax_why.v
/usr/share/doc/why/examples/misc/flag_why.sx
/usr/share/doc/why/examples/misc/flag_why.v
/usr/share/doc/why/examples/misc/gcd.mlw
/usr/share/doc/why/examples/misc/gcd_why.sx
/usr/share/doc/why/examples/misc/gcd_why.v
/usr/share/doc/why/examples/misc/loop0.mlw
/usr/share/doc/why/examples/misc/loop0_why.sx
/usr/share/doc/why/examples/misc/loop0_why.v
/usr/share/doc/why/examples/misc/mac_carthy.mlw
/usr/share/doc/why/examples/misc/mac_carthy_why.sx
/usr/share/doc/why/examples/misc/mac_carthy_why.v
/usr/share/doc/why/examples/misc/matrix.why
/usr/share/doc/why/examples/misc/matrix_mult.why
/usr/share/doc/why/examples/misc/matrix_why.v
/usr/share/doc/why/examples/misc/max.mlw
/usr/share/doc/why/examples/misc/max_why.sx
/usr/share/doc/why/examples/misc/max_why.v
/usr/share/doc/why/examples/misc/mix_max.mlw
/usr/share/doc/why/examples/misc/peano.mlw
/usr/share/doc/why/examples/misc/peano_why.sx
/usr/share/doc/why/examples/misc/peano_why.v
/usr/share/doc/why/examples/misc/power.mlw
/usr/share/doc/why/examples/misc/power_why.sx
/usr/share/doc/why/examples/misc/power_why.v
/usr/share/doc/why/examples/misc/search.mlw
/usr/share/doc/why/examples/misc/search_why.sx
/usr/share/doc/why/examples/misc/search_why.v
/usr/share/doc/why/examples/misc/sqrt_dicho.mlw
/usr/share/doc/why/examples/misc/sqrt_dicho_why.sx
/usr/share/doc/why/examples/misc/sqrt_dicho_why.v
/usr/share/doc/why/examples/misc/sum.mlw
/usr/share/doc/why/examples/misc/sum_why.sx
/usr/share/doc/why/examples/misc/sum_why.v
/usr/share/doc/why/examples/misc/swap0.mlw
/usr/share/doc/why/examples/misc/swap0_why.sx
/usr/share/doc/why/examples/misc/swap0_why.v
/usr/share/doc/why/examples/queens/.depend
/usr/share/doc/why/examples/queens/Makefile
/usr/share/doc/why/examples/queens/queens.why
/usr/share/doc/why/examples/queens/queens_why.v
/usr/share/doc/why/examples/quicksort/.depend
/usr/share/doc/why/examples/quicksort/Makefile
/usr/share/doc/why/examples/quicksort/Partition.v
/usr/share/doc/why/examples/quicksort/Quicksort.v
/usr/share/doc/why/examples/quicksort/partition.mlw
/usr/share/doc/why/examples/quicksort/partition_why.v
/usr/share/doc/why/examples/quicksort/quicksort.mlw
/usr/share/doc/why/examples/quicksort/quicksort_why.v
/usr/share/doc/why/examples/quicksort2/.depend
/usr/share/doc/why/examples/quicksort2/Makefile
/usr/share/doc/why/examples/quicksort2/quicksort2.mlw
/usr/share/doc/why/examples/quicksort2/quicksort2_why.sx
/usr/share/doc/why/examples/quicksort2/quicksort2_why.v
/usr/share/doc/why/examples/selectionsort/.depend
/usr/share/doc/why/examples/selectionsort/Makefile
/usr/share/doc/why/examples/selectionsort/selection.mlw
/usr/share/doc/why/examples/selectionsort/selection_why.sx
/usr/share/doc/why/examples/selectionsort/selection_why.v
/usr/share/doc/why/examples/sqrt/.depend
/usr/share/doc/why/examples/sqrt/Makefile
/usr/share/doc/why/examples/sqrt/simple.mlw
/usr/share/doc/why/examples/sqrt/simple_why.v
/usr/share/doc/why/examples/sqrt/sqrt.mlw
/usr/share/doc/why/examples/sqrt/sqrt_why.sx
/usr/share/doc/why/examples/sqrt/sqrt_why.v
/usr/share/doc/why/examples/string-matching/.depend
/usr/share/doc/why/examples/string-matching/Makefile
/usr/share/doc/why/examples/string-matching/Match.v
/usr/share/doc/why/examples/string-matching/brute_force_why.v
/usr/share/doc/why/examples/string-matching/not_so_naive_why.v

Changelog

2012-05-16 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-5) unstable; urgency=low
* Update 0001-Why-2.29-do-support-Coq-8.3.patch
- Mark Coq 8.3pl4 as compatible.
* Bump Standards-Version to 3.9.3, no changes required.
2012-04-06 - St├ęphane Glondu <glondu@debian.org>
why (2.30+dfsg-4) unstable; urgency=high
* Team upload
* Recompile with coq 8.3pl4 (no changes)
2012-01-16 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-3) unstable; urgency=high
* Fix 0002-Mark-alt-ergo-0.93-as-compatible.patch
- Adapt version_regexp because "alt-ergo -version" changed.
* Fix 0004-Default-to-why2-for-jessie-atp.patch
- default to "gui" instead of "why2".
* Add 0007-Replace-caduceus-invocation-by-Frama-C.patch
- Caduceus is gone. We use Frama-C instead.
- Adding Frama-C to Why's dependencies.
* Setting urgency to "high" to fix those issues.
2012-01-12 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-2) unstable; urgency=low
* Rebuilt with latest coq-float 1:8.3pl1-1 (no source changes).
2012-01-02 - Mehdi Dogguy <mehdi@debian.org>
why (2.30+dfsg-1) unstable; urgency=low
* New upstream release.
* Update patches:
- Rebase and update existing patches
- add 0004-Default-to-why2-for-jessie-atp.patch
- add 0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
* Add (back) Build-Depends on coq-float.
* Bump build requirement for frama-c to 20111001+nitrogen+dfsg-1~.
* Bump Standards-Version to 3.9.2, no changes needed.
* Fix description-synopsis-starts-with-article in why's description.
* Fix copyright-refers-to-deprecated-bsd-license-file
* Fix spelling-error-in-binary
* Mark Coq 8.3pl3 as compatible with current Why
2011-11-03 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-4) unstable; urgency=low
* Rebuild with OCaml 3.12.1.
2011-04-25 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-3) unstable; urgency=low
* Remove last added patch. The problem was in Makefile.dynamic, shipped
by frama-c-base which lacks some include statements.
- remove 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
- Bump minimum version number for Frama-C to 20110201+carbon+dfsg-2~.
2011-04-25 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-2) unstable; urgency=low
* Fix FTBFS on armel.
- add 0004-ocamlgraph-is-needed-to-link-frama-c-Jessie.patch
2011-04-24 - Mehdi Dogguy <mehdi@debian.org>
why (2.29+dfsg-1) unstable; urgency=low
* New upstream release.
- Remove old patches, which are not needed anymore.
- Remove build-depends on coq-float (upstream switched to Flocq which
is not packaged yet).
* Bump minimum version of Coq to 8.3
- and add 0001-Why-2.29-do-support-Coq-8.3.patch (upstream forgot to
mention to why-config that Coq 8.3 is "ok").
* Mark Alt-Ergo 0.93 as compatible
- add 0002-Mark-alt-ergo-0.93-as-compatible.patch
* Fix FTBFS due to non-exhaustive pattern matching
- add 0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
* Set 20110201+carbon+dfsg-1~ as minimum version number for Frama-C.
2011-03-11 - St├ęphane Glondu <glondu@debian.org>
why (2.26+dfsg-4) unstable; urgency=low
* Team upload
* Rebuild with coq 8.2.pl2+dfsg-2 (no changes)

See Also

Package Description
why_2.30+dfsg-5+b1_amd64.deb Software verification tool
whysynth_20090403-1.2_amd64.deb DSSI Soft Synth Interface
whyteboard_0.41.1-4_all.deb overlay painting and annotation application
wicd-cli_1.7.2.4-4_all.deb wired and wireless network manager - scriptable console client
wicd-curses_1.7.2.4-4_all.deb wired and wireless network manager - Curses client
wicd-daemon_1.7.2.4-4_all.deb wired and wireless network manager - daemon
wicd-gtk_1.7.2.4-4_all.deb wired and wireless network manager - GTK+ client
wicd-kde_0.3.0-2_amd64.deb Wired and wireless network manager - plasmoid
wicd_1.7.2.4-4_all.deb wired and wireless network manager - metapackage
wide-dhcpv6-client_20080615-11.1_amd64.deb DHCPv6 client for automatic IPv6 hosts configuration
wide-dhcpv6-relay_20080615-11.1_amd64.deb DHCPv6 relay for automatic IPv6 hosts configuration
wide-dhcpv6-server_20080615-11.1_amd64.deb DHCPv6 server for automatic IPv6 hosts configuration
widelands-data_17-3_all.deb fantasy real-time strategy game (data files)
widelands_17-3_amd64.deb fantasy real-time strategy game
widemargin_1.0.11-4_all.deb bible reading and study application
Advertisement
Advertisement