algo64: main program

6a83de46 · Jean-Christophe Filliâtre · dc8520ec · 6a83de46
Commit 6a83de46 authored Feb 07, 2014 by Jean-Christophe Filliâtre
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

examples/algo64.mlw examples/algo64.mlw +5 -0

No files found.
--- a/examples/algo64.mlw
+++ b/examples/algo64.mlw
@@ -49,4 +49,9 @@ module Algo64
      assert { permut_sub (at a 'L2) a m (n+1) }
    end

+  let qs (a:array int) : unit
+    ensures  { permut (old a) a }
+    ensures  { sorted a }
+  = if length a > 0 then quicksort a 0 (length a - 1)
+
 end