From af8564054c769d2ba9d748ab592d740e6cecfd5e Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Fri, 28 Mar 2014 22:18:56 +0100 Subject: [PATCH] mergesort_list: generic code, a bit of cleaning up --- examples/mergesort_list.mlw | 92 +- examples/mergesort_list/why3session.xml | 1497 ++++++++++++++++++----- 2 files changed, 1281 insertions(+), 308 deletions(-) diff --git a/examples/mergesort_list.mlw b/examples/mergesort_list.mlw index ea5aa0b5c..ea4bbbcdc 100644 --- a/examples/mergesort_list.mlw +++ b/examples/mergesort_list.mlw @@ -1,23 +1,82 @@ (* Sorting a list of integers using mergesort *) -module M +module Elt - use import int.Int - use import list.Length - use import list.SortedInt - use import list.Append - use import list.Permut + use export int.Int + use export list.Length + use export list.Append + use export list.Permut - let split (l0 : list 'a) + type elt + predicate le elt elt + clone relations.TotalPreOrder with type t = elt, predicate rel = le + clone export list.Sorted with type t = elt, predicate le = le + +end + +module Merge + + use export Elt + + let rec merge (l1 l2: list elt) : list elt + requires { sorted l1 /\ sorted l2 } + ensures { sorted result /\ permut result (l1 ++ l2) } + variant { length l1 + length l2 } + = match l1, l2 with + | Nil, _ -> l2 + | _, Nil -> l1 + | Cons x1 r1, Cons x2 r2 -> + if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) + end + +end + +(* TODO: proof to be completed +module EfficientMerge + + use export Elt + use import list.Mem + use import list.Reverse + use import list.RevAppend + + let rec merge_aux (acc l1 l2: list elt) : list elt + requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 } + requires { forall x y: elt. mem x acc -> mem y l1 -> le x y } + requires { forall x y: elt. mem x acc -> mem y l2 -> le x y } + ensures { sorted result /\ permut result (acc ++ l1 ++ l2) } + variant { length l1 + length l2 } + = match l1, l2 with + | Nil, _ -> rev_append acc l2 + | _, Nil -> rev_append acc l1 + | Cons x1 r1, Cons x2 r2 -> + if le x1 x2 then merge_aux (Cons x1 acc) r1 l2 + else merge_aux (Cons x2 acc) l1 r2 + end + + let merge (l1 l2: list elt) : list elt + requires { sorted l1 /\ sorted l2 } + ensures { sorted result /\ permut result (l1 ++ l2) } + = + merge_aux Nil l1 l2 + +end +*) + +module Mergesort + + use import Merge + + let split (l0: list 'a) : (list 'a, list 'a) requires { length l0 >= 2 } - ensures { let (l1, l2) = result in + ensures { let (l1, l2) = result in 1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) } - = let rec split_aux (l1 : list 'a) l2 l variant { length l } + = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a) requires { length l2 = length l1 \/ length l2 = length l1 + 1 } - ensures { let r1, r2 = result in + ensures { let r1, r2 = result in (length r2 = length r1 \/ length r2 = length r1 + 1) /\ permut (r1 ++ r2) (l1 ++ (l2 ++ l)) } + variant { length l } = match l with | Nil -> (l1, l2) | Cons x r -> split_aux l2 (Cons x l1) r @@ -25,18 +84,9 @@ module M in split_aux Nil Nil l0 - let rec merge l1 l2 variant { length l1 + length l2 } - requires { sorted l1 /\ sorted l2 } - ensures { sorted result /\ permut result (l1 ++ l2) } - = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons x1 r1, Cons x2 r2 -> - if x1 <= x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2) - end - - let rec mergesort l variant { length l } + let rec mergesort (l: list elt) : list elt ensures { sorted result /\ permut result l } + variant { length l } = match l with | Nil | Cons _ Nil -> l | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2) diff --git a/examples/mergesort_list/why3session.xml b/examples/mergesort_list/why3session.xml index 3306e1e02..0e0d88101 100644 --- a/examples/mergesort_list/why3session.xml +++ b/examples/mergesort_list/why3session.xml @@ -4,296 +4,1271 @@ + version="0.95.2"/> + name="CVC4" + version="1.3"/> + name="Spass" + version="3.7"/> - + version="4.3.1"/> + expanded="false"> + + + expanded="false" + shape="CCiapermutV7ainfix ++V0V1AasortedV7LaConsV2V6IapermutV6ainfix ++V0V3AasortedV6FAasortedV3AasortedV0Aainfix <ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1apermutV9ainfix ++V0V1AasortedV9LaConsV4V8IapermutV8ainfix ++V5V1AasortedV8FAasortedV1AasortedV5Aainfix <ainfix +alengthV5alengthV1ainfix +alengthV0alengthV1Aainfix <=c0ainfix +alengthV0alengthV1aleV4V2aConsVVapermutV1ainfix ++V0V1AasortedV1aNilV0aConsVVCapermutV1ainfix ++V0V1AasortedV1aNilapermutV0ainfix ++V0V1AasortedV0wV0aNilV1IasortedV1AasortedV0F"> + + + + + + - - + + + +