Proving the Correctness of an In-place Sorting Algorithm

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

Transcript

1. Proving the Correctness of an In-place Sorting Algorithm @myuon_myon
2. Author and Resources Twitter: @myuon_myon GitHub repository: myuon/verified-algo (Under proof construction!)
3. Extraction in Isabelle Extraction: definitions in proof assistant ➡ programs in practical language Isabelle supports: - Haskell - Scala - OCaml - SML
4. 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
5. 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!
6. 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) }
7. 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
8. 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
9. 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)
10. 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 () })
11. 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)"
12. Small-step V.S. Big-step Small-step: calculate “heap” bottom-up Big-step: find a “great enough” invariant condition
13. 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)"
14. - 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
15. Reference Thanks to HOL-Imperative! https://isabelle.in.tum.de/dist/library/HOL/HOL-Imperative_HOL/index.html