Binary Heaps in Why3
This is a Why3 version of the Binary Heaps example, from the VACID-0 benchmarks.
Authors: Claude Marché / Asma Tafat
Topics: Array Data Structure / Trees / Permutation / Data Structures
References: The VACID-0 Benchmarks
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
The source code is too large to be given on a single page.
The code,
its specification and the proofs are presented on the following
research
report:
Asma Tafat
and Claude Marché. Binary heaps formally verified in
why3. Research Report 7780, INRIA, October 2011.
The annotated code, the Why3 proof session file and the Coq proof script are available in the archive below.