diff options
| author |  Rustan Leino <unknown> | 2014-01-08 23:57:48 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-01-08 23:57:48 -0800 |
| commit | 5fcfcbe96910e4205e9777ca28405e4f48e0f120 (patch) | |
| tree | bb141a9d4e0245d257badfdf5fe2a36b0167bd0b /Test/dafny4/CoqArt-InsertionSort.dfy | |
| parent | de8338b233b3a4daec0f0cfcfeca59115e32e574 (diff) | |
Dafny renditions of sorting algorithms proved in other provers (Coq, Isabelle, F*)
Diffstat (limited to 'Test/dafny4/CoqArt-InsertionSort.dfy')
| -rw-r--r-- | Test/dafny4/CoqArt-InsertionSort.dfy | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/Test/dafny4/CoqArt-InsertionSort.dfy b/Test/dafny4/CoqArt-InsertionSort.dfy new file mode 100644 index 00000000..9ed57e98 --- /dev/null +++ b/Test/dafny4/CoqArt-InsertionSort.dfy @@ -0,0 +1,192 @@ +// Dafny transcription of the Coq development of insertion sort, as found in Coq'Art.
+
+datatype List<T> = Nil | Cons(head: T, tail: List)
+
+predicate sorted(l: List<int>)
+{
+ match l
+ case Nil => true
+ case Cons(x, rest) =>
+ match rest
+ case Nil => true
+ case Cons(y, _) => x <= y && sorted(rest)
+}
+
+lemma example_sort_2357()
+ ensures sorted(Cons(2, Cons(3, Cons(5, Cons(7, Nil)))));
+{
+}
+
+lemma sorted_inv(z: int, l: List<int>)
+ requires sorted(Cons(z, l));
+ ensures sorted(l);
+{
+ match l {
+ case Nil =>
+ case Cons(_, _) =>
+ }
+}
+
+// Number of occurrences of z in l
+function nb_occ(z: int, l: List<int>): nat
+{
+ match l
+ case Nil => 0
+ case Cons(z', l') =>
+ (if z == z' then 1 else 0) + nb_occ(z, l')
+}
+
+lemma example_nb_occ_0()
+ ensures nb_occ(3, Cons(3, Cons(7, Cons(3, Nil)))) == 2;
+{
+}
+
+lemma example_nb_occ_1()
+ ensures nb_occ(36725, Cons(3, Cons(7, Cons(3, Nil)))) == 0;
+{
+}
+
+// list l' is a permutation of list l
+predicate equiv(l: List<int>, l': List<int>)
+{
+ forall z :: nb_occ(z, l) == nb_occ(z, l')
+}
+
+// equiv is an equivalence
+lemma equiv_refl(l: List<int>)
+ ensures equiv(l, l);
+{
+}
+
+lemma equiv_sym(l: List<int>, l': List<int>)
+ requires equiv(l, l');
+ ensures equiv(l', l);
+{
+}
+
+lemma equiv_trans(l: List<int>, l': List<int>, l'': List<int>)
+ requires equiv(l, l') && equiv(l', l'');
+ ensures equiv(l, l'');
+{
+}
+
+lemma equiv_cons(z: int, l: List<int>, l': List<int>)
+ requires equiv(l, l');
+ ensures equiv(Cons(z, l), Cons(z, l'));
+{
+}
+
+lemma equiv_perm(a: int, b: int, l: List<int>, l': List<int>)
+ requires equiv(l, l');
+ ensures equiv(Cons(a, Cons(b, l)), Cons(b, Cons(a, l')));
+{
+ var L, L' := Cons(a, Cons(b, l)), Cons(b, Cons(a, l'));
+ forall z {
+ calc {
+ nb_occ(z, L);
+ (if z == a && z == b then 2 else if z == a || z == b then 1 else 0) + nb_occ(z, l);
+ (if z == a && z == b then 2 else if z == a || z == b then 1 else 0) + nb_occ(z, l');
+ nb_occ(z, L');
+ }
+ }
+}
+
+// insertion of z into l at the right place (assuming l is sorted)
+function method aux(z: int, l: List<int>): List<int>
+{
+ match l
+ case Nil => Cons(z, Nil)
+ case Cons(a, l') =>
+ if z <= a then Cons(z, l) else Cons(a, aux(z, l'))
+}
+
+lemma example_aux_0()
+ ensures aux(4, Cons(2, Cons(5, Nil))) == Cons(2, Cons(4, Cons(5, Nil)));
+{
+}
+
+lemma example_aux_1()
+ ensures aux(4, Cons(24, Cons(50, Nil))) == Cons(4, Cons(24, Cons(50, Nil)));
+{
+}
+
+// the aux function seems to be a good tool for sorting...
+
+lemma aux_equiv(l: List<int>, x: int)
+ ensures equiv(Cons(x, l), aux(x, l));
+{
+ match l {
+ case Nil =>
+ case Cons(_, _) =>
+ }
+}
+
+lemma aux_sorted(l: List<int>, x: int)
+ requires sorted(l);
+ ensures sorted(aux(x, l));
+{
+ match l {
+ case Nil =>
+ case Cons(_, l') =>
+ match l' {
+ case Nil =>
+ case Cons(_, _) =>
+ }
+ }
+}
+
+// the sorting function
+function sort(l: List<int>): List<int>
+ ensures var l' := sort(l); equiv(l, l') && sorted(l');
+{
+ existence_proof(l);
+ var l' :| equiv(l, l') && sorted(l'); l'
+}
+
+lemma existence_proof(l: List<int>)
+ ensures exists l' :: equiv(l, l') && sorted(l');
+{
+ match l {
+ case Nil =>
+ case Cons(x, m) =>
+ existence_proof(m);
+ var m' :| equiv(m, m') && sorted(m');
+ calc ==> {
+ equiv(m, m') && sorted(m');
+ equiv(l, Cons(x, m')) && sorted(m');
+ { aux_equiv(m', x); }
+ equiv(l, aux(x, m')) && sorted(m');
+ { aux_sorted(m', x); }
+ equiv(l, aux(x, m')) && sorted(aux(x, m'));
+ }
+ }
+}
+
+// to get a compilable function in Dafny
+function method Sort(l: List<int>): List<int>
+ ensures equiv(l, Sort(l)) && sorted(Sort(l));
+{
+ match l
+ case Nil => l
+ case Cons(x, m) =>
+ var m' := Sort(m);
+ assert equiv(l, Cons(x, m'));
+ aux_equiv(m', x);
+ aux_sorted(m', x);
+ aux(x, m')
+}
+
+predicate p_aux_equiv(l: List<int>, x: int)
+ ensures equiv(Cons(x, l), aux(x, l));
+{
+ aux_equiv(l, x);
+ true
+}
+
+predicate p_aux_sorted(l: List<int>, x: int)
+ requires sorted(l);
+ ensures sorted(aux(x, l));
+{
+ aux_sorted(l, x);
+ true
+}
|