Commit 97466b34 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: remove duplicate elements in an array using a mutable set

parent 1e2e8a98
(** {1 Removing duplicate elements in an array, using a mutable set}
Given an array [a] of size [n], returns a fresh array containing
the elements of [a] without duplicates, using a mutable set
(typically a hash table).
*)
(** {2 Specification} *)
module Spec
use export int.Int
use export array.Array
(** v appears in [a[0..s-1]] *)
predicate appears (v: 'a) (a: array 'a) (s: int) =
exists i: int. 0 <= i < s /\ a[i] = v
(** [a[0..s-1]] contains no duplicate element *)
predicate nodup (a: array 'a) (s: int) =
forall i: int. 0 <= i < s -> not (appears a[i] a i)
end
module MutableSet
use import set.Fset
type elt
type t = private { ghost mutable s: set elt }
val create () : t
ensures { is_empty result.s }
val add (t: t) (x: elt) : unit
writes { t.s }
ensures { t.s = add x (old t.s) }
val contains (t: t) (x: elt) : bool
ensures { result <-> mem x t.s }
val clear (t: t) : unit
writes { t.s }
ensures { is_empty t.s }
val size (t: t) : int
ensures { result = cardinal t.s }
end
(** {2 Quadratic implementation, without extra space} *)
module RemoveDuplicate
use import Spec
use import set.Fset
use import MutableSet
use import ref.Refint
use import array.Array
let remove_duplicate (a: array elt) : array elt
requires { 1 <= length a }
ensures { nodup result (length result) }
ensures { forall x: elt.
appears x a (length a) <-> appears x result (length result) }
=
let s = MutableSet.create () in
for i = 0 to Array.length a - 1 do
invariant { forall x: elt. appears x a i <-> mem x s.s }
MutableSet.add s a[i]
done;
'L:
let r = Array.make (MutableSet.size s) a[0] in
MutableSet.clear s;
let j = ref 0 in
for i = 0 to Array.length a - 1 do
invariant { forall x: elt. appears x a i <-> mem x s.s }
invariant { forall x: elt. mem x s.s <-> appears x r !j }
invariant { nodup r !j }
invariant { 0 <= !j = cardinal s.s <= length r }
invariant { subset s.s (at s.s 'L) }
if not (MutableSet.contains s a[i]) then begin
MutableSet.add s a[i];
r[!j] <- a[i];
incr j
end
done;
r
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="0.99.1" timelimit="6" memlimit="1000"/>
<file name="../remove_duplicate_hash.mlw" expanded="true">
<theory name="Spec" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MutableSet" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="RemoveDuplicate" sum="170bcbe1f13bb097aaf05b4437fedcda">
<goal name="WP_parameter remove_duplicate" expl="VC for remove_duplicate">
<transf name="split_goal_wp">
<goal name="WP_parameter remove_duplicate.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.2" expl="2. array creation size">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.5" expl="5. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.6" expl="6. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.7" expl="7. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.8" expl="8. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.9" expl="9. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.10" expl="10. index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.11" expl="11. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.12" expl="12. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.13" expl="13. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.14" expl="14. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.15" expl="15. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.16" expl="16. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.06" steps="23"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.18" expl="18. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.19" expl="19. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.20" expl="20. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.00" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.21" expl="21. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.23" expl="23. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.24" expl="24. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.00" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.25" expl="25. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.26" expl="26. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.27" expl="27. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.28" expl="28. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.29" expl="29. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.30" expl="30. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.31" expl="31. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.32" expl="32. array creation size">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.33" expl="33. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.34" expl="34. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.35" expl="35. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.36" expl="36. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.37" expl="37. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.38" expl="38. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.39" expl="39. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.40" expl="40. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.41" expl="41. index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.42" expl="42. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.43" expl="43. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.44" expl="44. index in array bounds">
<transf name="split_goal_wp">
<goal name="WP_parameter remove_duplicate.44.1" expl="1. VC for remove_duplicate">
<proof prover="0"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.44.2" expl="2. VC for remove_duplicate">
<proof prover="0"><result status="valid" time="0.04" steps="79"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter remove_duplicate.45" expl="45. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="121"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.46" expl="46. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.17" steps="237"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.47" expl="47. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.21" steps="188"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.48" expl="48. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.49" expl="49. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.50" expl="50. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="56"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.51" expl="51. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.52" expl="52. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.53" expl="53. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.54" expl="54. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.55" expl="55. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.56" expl="56. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="96"/></proof>
</goal>
<goal name="WP_parameter remove_duplicate.57" expl="57. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="185"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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