new example: gnome sort

parent c9e631c0
(* Gnome sort
https://en.wikipedia.org/wiki/Gnome_sort
*)
module GnomeSort
use import int.Int
use import ref.Refint
use import array.Array
use import array.ArrayPermut
use import array.IntArraySorted
use import array.ArraySwap
use import array.Inversions
let gnome_sort (a: array int) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= let pos = ref 0 in
while !pos < length a do
invariant { 0 <= !pos <= length a }
invariant { sorted_sub a 0 !pos }
invariant { permut_all (old a) a }
variant { inversions a, length a - !pos }
if !pos = 0 || a[!pos] >= a[!pos - 1] then
incr pos
else begin
swap a !pos (!pos - 1);
decr pos
end
done
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gnome_sort.mlw" expanded="true">
<theory name="GnomeSort" sum="a298d63bf73b885c8b6729130e79acb8" expanded="true">
<goal name="VC gnome_sort" expl="VC for gnome_sort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC gnome_sort.1" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC gnome_sort.2" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC gnome_sort.3" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC gnome_sort.4" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.5" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.6" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC gnome_sort.7" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.8" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="43"/></proof>
</goal>
<goal name="VC gnome_sort.9" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC gnome_sort.10" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC gnome_sort.11" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="VC gnome_sort.12" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC gnome_sort.13" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="VC gnome_sort.14" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.05" steps="89"/></proof>
</goal>
<goal name="VC gnome_sort.15" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC gnome_sort.16" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -7,7 +7,8 @@ module Intf
ghost mutable repr: int -> int;
} invariant {
0 <= size /\
forall i. 0 <= i < size -> 0 <= repr i < size
(forall i. 0 <= i < size -> 0 <= repr i < size) /\
(forall i. 0 <= i < size -> repr (repr i) = repr i)
} by { size = 0; repr = fun i -> i }
val create (n: int) : t
......@@ -113,9 +114,8 @@ module Impl
if y <> x then begin
assert { path uf.size uf.link y (uf.dist x - 1) (uf.repr x) };
let r = find uf y in
(* path compression *)
assert { x <> r };
uf.link[x] <- r;
uf.link[x] <- r; (* path compression *)
uf.dist <- pure { fun i -> if i = x then 1
else if exists d. path uf.size uf.link i d x then uf.dist i + 1
else uf.dist i };
......
......@@ -114,8 +114,8 @@
<goal name="VC create" expl="VC for create">
<proof prover="0"><result status="valid" time="0.01" steps="98"/></proof>
</goal>
<goal name="VC find" expl="VC for find">
<transf name="split_goal_wp">
<goal name="VC find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC find.1" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
......@@ -141,8 +141,8 @@
<goal name="VC find.6" expl="index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
</goal>
<goal name="VC find.7" expl="type invariant">
<transf name="split_goal_wp">
<goal name="VC find.7" expl="type invariant" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC find.7.1" expl="VC for find">
<proof prover="0"><result status="valid" time="0.00" steps="31"/></proof>
</goal>
......
......@@ -14,14 +14,13 @@ Author: Jean-Christophe Filliâtre (CNRS)
module Challenge3
use import int.Int
use import int.Sum
use import int.NumOf
use import int.ComputerDivision
use import ref.Refint
use import array.Array
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.Inversions
(* odd-sorted up to n exclusive *)
predicate odd_sorted (a: array int) (n: int) =
......@@ -45,72 +44,6 @@ module Challenge3
i-1 = 2 * div (i-1) 2 + 1 }
done
(* to prove termination, we count the total number of inversions *)
predicate inversion (a: array int) (i j: int) =
a[i] > a[j]
function inversions_for (a: array int) (i: int) : int =
numof (inversion a i) i (length a)
function inversions (a: array int) : int =
sum (inversions_for a) 0 (length a)
(* the key lemma to prove termination: whenever we swap two consecutive
values that are ill-sorted, the total number of inversions decreases *)
let lemma exchange_inversion (a1 a2: array int) (i0: int)
requires { 0 <= i0 < length a1 - 1 }
requires { a1[i0] > a1[i0 + 1] }
requires { exchange a1 a2 i0 (i0 + 1) }
ensures { inversions a2 < inversions a1 }
= assert { inversion a1 i0 (i0+1) };
assert { not (inversion a2 i0 (i0+1)) };
assert { forall i. 0 <= i < i0 ->
inversions_for a2 i = inversions_for a1 i
by numof (inversion a2 i) i (length a2)
= numof (inversion a2 i) i i0
+ numof (inversion a2 i) i0 (i0+1)
+ numof (inversion a2 i) (i0+1) (i0+2)
+ numof (inversion a2 i) (i0+2) (length a2)
/\ numof (inversion a1 i) i (length a1)
= numof (inversion a1 i) i i0
+ numof (inversion a1 i) i0 (i0+1)
+ numof (inversion a1 i) (i0+1) (i0+2)
+ numof (inversion a1 i) (i0+2) (length a1)
/\ numof (inversion a2 i) i0 (i0+1)
= numof (inversion a1 i) (i0+1) (i0+2)
/\ numof (inversion a2 i) (i0+1) (i0+2)
= numof (inversion a1 i) i0 (i0+1)
/\ numof (inversion a2 i) i i0 = numof (inversion a1 i) i i0
/\ numof (inversion a2 i) (i0+2) (length a2)
= numof (inversion a1 i) (i0+2) (length a1)
};
assert { forall i. i0 + 1 < i < length a1 ->
inversions_for a2 i = inversions_for a1 i };
assert { inversions_for a2 i0 = inversions_for a1 (i0+1)
by numof (inversion a1 (i0+1)) (i0+2) (length a1)
= numof (inversion a2 i0 ) (i0+2) (length a1) };
assert { 1 + inversions_for a2 (i0+1) = inversions_for a1 i0
by numof (inversion a1 i0) i0 (length a1)
= numof (inversion a1 i0) (i0+1) (length a1)
= 1 + numof (inversion a1 i0) (i0+2) (length a1) };
let sum_decomp (a: array int) (i j k: int)
requires { 0 <= i <= j <= k <= length a = length a1 }
ensures { sum (inversions_for a) i k =
sum (inversions_for a) i j + sum (inversions_for a) j k }
= () in
let decomp (a: array int)
requires { length a = length a1 }
ensures { inversions a = sum (inversions_for a) 0 i0
+ inversions_for a i0
+ inversions_for a (i0+1)
+ sum (inversions_for a) (i0+2) (length a) }
= sum_decomp a 0 i0 (length a);
sum_decomp a i0 (i0+1) (length a);
sum_decomp a (i0+1) (i0+2) (length a);
in
decomp a1; decomp a2;
()
(* note: program variable "sorted" renamed into "is_sorted"
(clash with library predicate "sorted" on arrays) *)
let odd_even_transposition_sort (a: array int)
......
......@@ -3,10 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../verifythis_2017_odd_even_transposition_sort.mlw">
<theory name="Challenge3" sum="09b9c859f19063fb3660a5d562dc71ae">
<file name="../verifythis_2017_odd_even_transposition_sort.mlw" expanded="true">
<theory name="Challenge3" sum="46e80290f8c8bc8c5532de2fa9ab2ffa" expanded="true">
<goal name="VC odd_even_sorted" expl="VC for odd_even_sorted">
<transf name="split_goal_wp">
<goal name="VC odd_even_sorted.1" expl="loop invariant init">
......@@ -33,100 +32,6 @@
</goal>
</transf>
</goal>
<goal name="VC exchange_inversion" expl="VC for exchange_inversion">
<transf name="split_goal_wp">
<goal name="VC exchange_inversion.1" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC exchange_inversion.2" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC exchange_inversion.3" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC exchange_inversion.3.1" expl="assertion">
<proof prover="1"><result status="valid" time="1.33"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC exchange_inversion.3.2" expl="assertion">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC exchange_inversion.3.3" expl="assertion">
<proof prover="0"><result status="valid" time="1.32" steps="1134"/></proof>
</goal>
<goal name="VC exchange_inversion.3.4" expl="assertion">
<proof prover="0"><result status="valid" time="0.63" steps="636"/></proof>
</goal>
<goal name="VC exchange_inversion.3.5" expl="assertion">
<proof prover="2" timelimit="35"><result status="valid" time="28.90"/></proof>
</goal>
<goal name="VC exchange_inversion.3.6" expl="assertion">
<proof prover="2"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="VC exchange_inversion.3.7" expl="VC for exchange_inversion">
<transf name="introduce_premises">
<goal name="VC exchange_inversion.3.7.1" expl="VC for exchange_inversion">
<transf name="inline_goal">
<goal name="VC exchange_inversion.3.7.1.1" expl="VC for exchange_inversion">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC exchange_inversion.4" expl="assertion">
<proof prover="2"><result status="valid" time="1.81"/></proof>
</goal>
<goal name="VC exchange_inversion.5" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC exchange_inversion.5.1" expl="VC for exchange_inversion">
<proof prover="2"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="VC exchange_inversion.5.2" expl="VC for exchange_inversion">
<proof prover="0"><result status="valid" time="1.77" steps="851"/></proof>
</goal>
</transf>
</goal>
<goal name="VC exchange_inversion.6" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC exchange_inversion.6.1" expl="VC for exchange_inversion">
<proof prover="0"><result status="valid" time="0.08" steps="156"/></proof>
</goal>
<goal name="VC exchange_inversion.6.2" expl="VC for exchange_inversion">
<proof prover="0"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="VC exchange_inversion.6.3" expl="VC for exchange_inversion">
<proof prover="2"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
</goal>
<goal name="VC exchange_inversion.7" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC exchange_inversion.8" expl="precondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="VC exchange_inversion.9" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC exchange_inversion.10" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="VC exchange_inversion.11" expl="postcondition">
<proof prover="0"><result status="valid" time="0.13" steps="44"/></proof>
</goal>
<goal name="VC exchange_inversion.12" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="VC exchange_inversion.13" expl="precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC exchange_inversion.14" expl="postcondition">
<proof prover="2"><result status="valid" time="0.69"/></proof>
</goal>
</transf>
</goal>
<goal name="VC odd_even_transposition_sort" expl="VC for odd_even_transposition_sort">
<transf name="split_goal_wp">
<goal name="VC odd_even_transposition_sort.1" expl="loop invariant init">
......@@ -229,16 +134,16 @@
<proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="VC odd_even_transposition_sort.34" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.13" steps="398"/></proof>
<proof prover="0"><result status="valid" time="0.25" steps="398"/></proof>
</goal>
<goal name="VC odd_even_transposition_sort.35" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC odd_even_transposition_sort.36" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.21" steps="285"/></proof>
<proof prover="0"><result status="valid" time="0.21" steps="366"/></proof>
</goal>
<goal name="VC odd_even_transposition_sort.37" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.04" steps="226"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="243"/></proof>
</goal>
<goal name="VC odd_even_transposition_sort.38" expl="loop invariant preservation">
<proof prover="0"><result status="valid" time="0.08" steps="49"/></proof>
......
......@@ -357,3 +357,85 @@ module ToSeq
meta coercion function to_seq
end
(** {2 Number of inversions in an array of integers}
We show that swapping two elements that are ill-sorted decreases
the number of inversions. Useful to prove the termination of
sorting algorithms that use swaps. *)
module Inversions
use import Array
use import ArrayExchange
use import int.Int
use import int.Sum
use import int.NumOf
(* to prove termination, we count the total number of inversions *)
predicate inversion (a: array int) (i j: int) =
a[i] > a[j]
function inversions_for (a: array int) (i: int) : int =
numof (inversion a i) i (length a)
function inversions (a: array int) : int =
sum (inversions_for a) 0 (length a)
(* the key lemma to prove termination: whenever we swap two consecutive
values that are ill-sorted, the total number of inversions decreases *)
let lemma exchange_inversion (a1 a2: array int) (i0: int)
requires { 0 <= i0 < length a1 - 1 }
requires { a1[i0] > a1[i0 + 1] }
requires { exchange a1 a2 i0 (i0 + 1) }
ensures { inversions a2 < inversions a1 }
= assert { inversion a1 i0 (i0+1) };
assert { not (inversion a2 i0 (i0+1)) };
assert { forall i. 0 <= i < i0 ->
inversions_for a2 i = inversions_for a1 i
by numof (inversion a2 i) i (length a2)
= numof (inversion a2 i) i i0
+ numof (inversion a2 i) i0 (i0+1)
+ numof (inversion a2 i) (i0+1) (i0+2)
+ numof (inversion a2 i) (i0+2) (length a2)
/\ numof (inversion a1 i) i (length a1)
= numof (inversion a1 i) i i0
+ numof (inversion a1 i) i0 (i0+1)
+ numof (inversion a1 i) (i0+1) (i0+2)
+ numof (inversion a1 i) (i0+2) (length a1)
/\ numof (inversion a2 i) i0 (i0+1)
= numof (inversion a1 i) (i0+1) (i0+2)
/\ numof (inversion a2 i) (i0+1) (i0+2)
= numof (inversion a1 i) i0 (i0+1)
/\ numof (inversion a2 i) i i0 = numof (inversion a1 i) i i0
/\ numof (inversion a2 i) (i0+2) (length a2)
= numof (inversion a1 i) (i0+2) (length a1)
};
assert { forall i. i0 + 1 < i < length a1 ->
inversions_for a2 i = inversions_for a1 i };
assert { inversions_for a2 i0 = inversions_for a1 (i0+1)
by numof (inversion a1 (i0+1)) (i0+2) (length a1)
= numof (inversion a2 i0 ) (i0+2) (length a1) };
assert { 1 + inversions_for a2 (i0+1) = inversions_for a1 i0
by numof (inversion a1 i0) i0 (length a1)
= numof (inversion a1 i0) (i0+1) (length a1)
= 1 + numof (inversion a1 i0) (i0+2) (length a1) };
let sum_decomp (a: array int) (i j k: int)
requires { 0 <= i <= j <= k <= length a = length a1 }
ensures { sum (inversions_for a) i k =
sum (inversions_for a) i j + sum (inversions_for a) j k }
= () in
let decomp (a: array int)
requires { length a = length a1 }
ensures { inversions a = sum (inversions_for a) 0 i0
+ inversions_for a i0
+ inversions_for a (i0+1)
+ sum (inversions_for a) (i0+2) (length a) }
= sum_decomp a 0 i0 (length a);
sum_decomp a i0 (i0+1) (length a);
sum_decomp a (i0+1) (i0+2) (length a);
in
decomp a1; decomp a2;
()
end
module MapOcc
use import int.Int
use import map.Map
use import map.Occ
lemma occ_exchange :
forall m: map int 'a, l u i j: int, x y z: 'a.
l <= i < u ->
l <= j < u ->
Occ.occ z m[i <- x][j <- y] l u =
Occ.occ z m[i <- y][j <- x] l u
end
module Python
use import int.Int
......@@ -47,10 +34,10 @@ module Python
(* ad-hoc facts about exchange *)
use MapOcc
use import map.Occ
function occurrence (v: 'a) (l: list 'a) : int =
MapOcc.Occ.occ v l.Array.elts 0 l.Array.length
Occ.occ v l.Array.elts 0 l.Array.length
(* Python's division and modulus according are neither Euclidean division,
nor computer division, but something else defined in
......
......@@ -156,6 +156,12 @@ theory Occ
(forall i: int. l <= i < u -> m1[i] = m2[i]) -> occ v m1 l u = occ v m2 l u
(* by induction on u *)
lemma occ_exchange :
forall m: map int 'a, l u i j: int, x y z: 'a.
l <= i < u -> l <= j < u ->
occ z m[i <- x][j <- y] l u =
occ z m[i <- y][j <- x] l u
end
theory MapPermut
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment