Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Proving the Correctness of an In-place Sorting ...

myuon
March 02, 2019

Proving the Correctness of an In-place Sorting Algorithm

#静的コード解析の会 第9回 発表資料

myuon

March 02, 2019
Tweet

More Decks by myuon

Other Decks in Technology

Transcript

  1. Extraction in Isabelle Extraction: definitions in proof assistant ➡ programs

    in practical language Isabelle supports: - Haskell - Scala - OCaml - SML
  2. Sorting Algorithm? Currently, I’m working on “Selection Sort” Pseudo-code: for

    I := 1 to N min := I for J := I+1 to N if data[J] < data[min] then min := J end if end for swap(data[I], data[min]) end for
  3. How to prove the correctness? But the algorithm is in-place!

    1. Rewrite the algorithm into a pure and non IO effect one ◦ Usually difficult ◦ How to guarantee the equality of the algorithms? 2. Prove it directly ◦ Simple, but how to handle variables and arrays? ◦ ➡ IO monad!
  4. Isabelle Monad Syntax Using “HOL-Library/Monad_Syntax”, we have do-notation! (and the

    bind ‘>>=’ too) do { valJ ← read arr j; m ← ! min_ref; valMin ← read arr m; whenu (valJ < valMin) (min_ref := j) }
  5. Reinvent the IO wheel datatype 'a io = IO "heap

    ⇒ ('a × heap)" primrec execute :: "'a io ⇒ heap ⇒ ('a × heap)" where [code del]: "execute (IO f) = f" - IO monad as a state monad of heap - “heap” means memory state (variables and arrays are there) - Normal memory operations can be defined, including allocate, read and write
  6. Ref types Ref type - ‘a ref means some reference

    to the value whose type is ‘a - Operators (all are in IO context): - ref x: allocate a new cell and initialize by the value x - ! r: read the value - r := v: write the value v into the ref r
  7. A bit about arrays Mutable Arrays - Consists of a

    pointer (to the head) and a number (length) - A successive sequent cells in memory - If out of the index... ➡ undefined (ignore error here)
  8. In-place Selection Sort in IO monad let n = size_of_mvector

    arr in forMu [0..<n] (λi. do { min_ref ← ref i; forMu [i+1..<n] (λj. do { valJ ← read arr j; m ← ! min_ref; valMin ← read arr m; whenu (valJ < valMin) (min_ref := j) }); m ← ! min_ref; swap arr i m; return () })
  9. Sortedness Statement Statement: the result array of the algorithm is

    “sorted” - Allocate an array and initialize using given list - Do the sort - Read the array and check if it’s sorted primrec sorted :: "'a::ord list ⇒ bool" where "sorted [] = True" | "sorted (x#xs) = ((∀y∈set xs. x ≤ y) ∧ sorted xs)"
  10. Small-step Observation - The statement tend to become super complex

    as the program become long - One way and never go wrong (when calculation has done) lemma assumes "effect program h h' r" shows "h' = super_complex_calculation(h)" and "r = super_complex_function(r)"
  11. - Proof looks great, sophisticated and gorgeous - Usually difficult

    (need a gut) - Sometimes many ways to go ahead - “loop invariant condition”, or more generally, “program invariant condition” lemma assumes "P (forM [] program)" and "\forall i. P (forM (take i xs) program) ==> P (forM (take (i+1) xs) program)" shows "P (forM xs program)" Big-step Observation