Reasoning about an imperative proto-language. Ending with a proof that insertionsort always finishes and returns a list which is sorted and it is a permutation of the input.
coqdoc
  • set, setandraise and some facts Things about lists to use in programming or to prove insertionsort.
    coqdoc
  • Definition of an imperative proto-language
    coqdoc
  • program concatenation, postcondition, finishing
    coqdoc
  • Definition of insertionsort and proof that it sorts a list
    coqdoc