Sorting algorithms

  • Selection sort (proof1, proof2)

  • Bubble sort (proof1, proof2)

  • Insertion sort (proof1, proof2; proof3). Stability (proof4)

  • Insertion sort in lists (proof1, proof2)

  • Insertion in sorted trees (proof1, proof2).

  • Quicksort (proof, coq1, coq2)

  • Mergesort on lists (proof1, proof2)

  • Mergesort (proof1, proof2; coq1, coq2 )

    Graph algorithms

  • GraphSet module (proof)

  • Abstract depth first search (white initial color) (proof1, proof2; proof3, proof4)

  • Abstract depth first search (proof == sound + complete)

  • Abstract depth first search [with black and gray sets] (proof == sound + complete)

  • Abstract DFS: no white to black edge for undirected graph (proof)
     

  • Random search walk (sound + complete; sound2)

  • Breadth first search (sound, complete)

  • Iterative depth first search with a stack (sound, complete)
     

  • Depth first search (mutable visited set) (sound, complete)

  • Depth first search (list of vertices + mutable visited set) (sound, complete)

  • Depth first search (list of vertices + mutable visited set + color) (sound, complete)

  • Depth first search as in Sedgewick (sound, complete; with graph array sound; complete)
     

  • Strongly connected components - Tarjan 1972 (abs) (proof1, proof2, proof3)

  • Strongly connected components - Tarjan 1972 (quasi imperative) (proof)

  • Strongly connected components - Kosaraju 1978 (abs) (proof)

  • Acyclicity test (functional, imperative)




     
    Jean-Jacques Lévy
    Chen Ran

    
    

  • Generated by why3doc 0.83