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)

  • The white-path theorem for depth first search (proof == sound + complete)

  • The white-path theorem for 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 (with ranks and explicit grays) (proof1)

  • SCC - Tarjan 1972 (with just ranks) (weak, strong)

  • SCC - Tarjan 1972 (with precedes) (weak, strong) [ a ]

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

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

  • Articulation points (weak, strong)

  • Biconnected components (weak, strong)

  • Acyclicity test (functional, imperative)
     




     
    Jean-Jacques Lévy
    Chen Ran

    
    

  • Generated by why3doc 0.83