This page collects several programs verified using Why version 2.xx. It is considered obsolete.

External proofs

• Knuth's algorithm for prime number based on Bertrand's postulate: available here (code and proof by Laurent Théry)

• A proof of GMP square root: available here (code and proof by Nicolas Magaud)

Examples contained in Why distribution

Note : Most Coq proofs require Coq 7.4.

• Dijkstra's Dutch national flag
  • Source: flag.mlw
  • Coq proof: flag_why.v / Index

• Levenshtein distance (code by Claude Marché)
  • Source: distance.mlw
  • Coq proof: words.v / distance_why.v / Index

• Bresenham line drawing algorithm (proof of optimality)
  • Source: bresenham.mlw
  • Coq proof: zaux.v / bresenham_why.v / Index

• Binary search
  • Source: bsearch.mlw
  • Coq proof: bsearch_why.v / Index

• Integer square root (code and proof by Claude Marché)
  • Source: sqrt.mlw
  • Coq proof: sqrt_why.v / Index

• Mac Carthy's 91 function
  • Source: mac_carthy.mlw
  • Coq proof: mac_carthy_why.v / Index

• Knuth-Morris-Pratt string searching algorithm
  • Source: kmp.mlw
  • Coq proof: Lex.v / Match.v / Next.v / kmp_why.v / Index

• Find, from this article: C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, Jan 1971.
  • Source: find.mlw
  • Coq proof: find_spec.v / find_lemmas.v / find_proofs.v / find_why.v / Index
  • The Coq proof is detailed in this paper

Sorting algorithms

• Maximum sort (code and proof by Sylvain Boulmé)
  • Source: maximumsort.mlw
  • Coq proof: maximumsort_why.v / Index

• Selection sort
  • Source: selection.mlw
  • Coq proof: selection_why.v / Index

• Quicksort
  • Source: partition.mlw / quicksort.mlw
  • Coq proof: Partition.v / Quicksort.v / partition_why.v / quicksort_why.v / Index
  • The proof is detailed in this paper

• Quicksort : a variant with a simpler partitioning, from Bentley's Programming Pearls
  • Source: quicksort2.mlw
  • Coq proof: quicksort2_why.v / Index

• Heapsort (in place)
  • Source: swap.mlw / downheap.mlw / heapsort.mlw
  • Coq proof: heap.v / Inftree.v / swap_why.v / downheap_why.v / heapsort_why.v / Index
  • The proof is detailed in this paper