From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 12 Aug 2015 22:44:50 -0700 Subject: Change the induction heuristic for lemmas to also look in precondition for clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others. --- Test/dafny3/Filter.dfy | 16 ++++++------- Test/dafny3/GenericSort.dfy | 56 +++++++++++++++++++++---------------------- Test/dafny3/InfiniteTrees.dfy | 44 ++++++++++------------------------ 3 files changed, 48 insertions(+), 68 deletions(-) (limited to 'Test/dafny3') diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index 24c8e94e..6e67de26 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -35,7 +35,7 @@ lemma Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat) // this lemma could ha { if k != 0 { Lemma_InTail(s.head, u); - Lemma_TailSubStreamK(s.tail, u, k-1); + //Lemma_TailSubStreamK(s.tail, u, k-1); } } lemma Lemma_InSubStream(x: T, s: Stream, u: Stream) @@ -193,10 +193,10 @@ lemma FS_Ping(s: Stream, h: PredicateHandle, x: T) } lemma FS_Pong(s: Stream, h: PredicateHandle, x: T, k: nat) - requires AlwaysAnother(s, h) && In(x, s) && P(x, h); - requires Tail(s, k).head == x; - ensures In(x, Filter(s, h)); - decreases k; + requires AlwaysAnother(s, h) && In(x, s) && P(x, h) + requires Tail(s, k).head == x + ensures In(x, Filter(s, h)) + decreases k { var fs := Filter(s, h); if s.head == x { @@ -205,14 +205,14 @@ lemma FS_Pong(s: Stream, h: PredicateHandle, x: T, k: nat) assert fs == Cons(s.head, Filter(s.tail, h)); // reminder of where we are calc { true; - == { FS_Pong(s.tail, h, x, k-1); } + //== { FS_Pong(s.tail, h, x, k-1); } In(x, Filter(s.tail, h)); ==> { assert fs.head != x; Lemma_InTail(x, fs); } In(x, fs); } } else { - assert fs == Filter(s.tail, h); // reminder of where we are - FS_Pong(s.tail, h, x, k-1); + //assert fs == Filter(s.tail, h); // reminder of where we are + //FS_Pong(s.tail, h, x, k-1); } } diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 7ea038be..6bd06965 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -7,25 +7,25 @@ abstract module TotalOrder { // Three properties of total orders. Here, they are given as unproved // lemmas, that is, as axioms. lemma Antisymmetry(a: T, b: T) - requires Leq(a, b) && Leq(b, a); - ensures a == b; + requires Leq(a, b) && Leq(b, a) + ensures a == b lemma Transitivity(a: T, b: T, c: T) - requires Leq(a, b) && Leq(b, c); - ensures Leq(a, c); + requires Leq(a, b) && Leq(b, c) + ensures Leq(a, c) lemma Totality(a: T, b: T) - ensures Leq(a, b) || Leq(b, a); + ensures Leq(a, b) || Leq(b, a) } abstract module Sort { import O as TotalOrder // let O denote some module that has the members of TotalOrder predicate Sorted(a: array, low: int, high: int) - requires a != null && 0 <= low <= high <= a.Length; - reads a; + requires a != null && 0 <= low <= high <= a.Length + reads a // The body of the predicate is hidden outside the module, but the postcondition is // "exported" (that is, visible, known) outside the module. Here, we choose the // export the following property: - ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]); + ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]) { forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]) } @@ -33,18 +33,18 @@ abstract module Sort { // In the insertion sort routine below, it's more convenient to keep track of only that // neighboring elements of the array are sorted... predicate NeighborSorted(a: array, low: int, high: int) - requires a != null && 0 <= low <= high <= a.Length; - reads a; + requires a != null && 0 <= low <= high <= a.Length + reads a { forall i :: low < i < high ==> O.Leq(a[i-1], a[i]) } // ...but we show that property to imply all pairs to be sorted. The proof of this // lemma uses the transitivity property. lemma NeighborSorted_implies_Sorted(a: array, low: int, high: int) - requires a != null && 0 <= low <= high <= a.Length; - requires NeighborSorted(a, low, high); - ensures Sorted(a, low, high); - decreases high - low; + requires a != null && 0 <= low <= high <= a.Length + requires NeighborSorted(a, low, high) + ensures Sorted(a, low, high) + decreases high - low { if low != high { NeighborSorted_implies_Sorted(a, low+1, high); @@ -57,25 +57,25 @@ abstract module Sort { // Standard insertion sort method method InsertionSort(a: array) - requires a != null; - modifies a; - ensures Sorted(a, 0, a.Length); - ensures multiset(a[..]) == old(multiset(a[..])); + requires a != null + modifies a + ensures Sorted(a, 0, a.Length) + ensures multiset(a[..]) == old(multiset(a[..])) { if a.Length == 0 { return; } var i := 1; while i < a.Length - invariant 0 < i <= a.Length; - invariant NeighborSorted(a, 0, i); - invariant multiset(a[..]) == old(multiset(a[..])); + invariant 0 < i <= a.Length + invariant NeighborSorted(a, 0, i) + invariant multiset(a[..]) == old(multiset(a[..])) { var j := i; while 0 < j && !O.Leq(a[j-1], a[j]) - invariant 0 <= j <= i; - invariant NeighborSorted(a, 0, j); - invariant NeighborSorted(a, j, i+1); - invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1]); - invariant multiset(a[..]) == old(multiset(a[..])); + invariant 0 <= j <= i + invariant NeighborSorted(a, 0, j) + invariant NeighborSorted(a, j, i+1) + invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1]) + invariant multiset(a[..]) == old(multiset(a[..])) { // The proof of correctness uses the totality property here. // It implies that if two elements are not previously in @@ -97,7 +97,7 @@ module IntOrder refines TotalOrder { datatype T = Int(i: int) // Define the ordering on these integers predicate method Leq ... - ensures Leq(a, b) ==> a.i <= b.i; + ensures Leq(a, b) ==> a.i <= b.i { a.i <= b.i } @@ -156,7 +156,7 @@ module intOrder refines TotalOrder { type T = int // Define the ordering on these integers predicate method Leq ... - ensures Leq(a, b) ==> a <= b; + ensures Leq(a, b) ==> a <= b { a <= b } diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy index 516a9e4e..85f73bc3 100644 --- a/Test/dafny3/InfiniteTrees.dfy +++ b/Test/dafny3/InfiniteTrees.dfy @@ -286,7 +286,7 @@ lemma Theorem1_Lemma(t: Tree, n: nat, p: Stream) LowerThan(ch, n); ==> // def. LowerThan LowerThan(ch.head.children, n-1); - ==> { Theorem1_Lemma(ch.head, n-1, tail); } + ==> //{ Theorem1_Lemma(ch.head, n-1, tail); } !IsNeverEndingStream(tail); ==> // def. IsNeverEndingStream !IsNeverEndingStream(p); @@ -374,30 +374,30 @@ lemma Proposition3b() } } lemma Proposition3b_Lemma(t: Tree, h: nat, p: Stream) - requires LowerThan(t.children, h) && ValidPath(t, p); - ensures !IsNeverEndingStream(p); - decreases h; + requires LowerThan(t.children, h) && ValidPath(t, p) + ensures !IsNeverEndingStream(p) + decreases h { match p { case Nil => case Cons(index, tail) => // From the definition of ValidPath(t, p), we get the following: var ch := Tail(t.children, index); - assert ch.Cons? && ValidPath(ch.head, tail); + // assert ch.Cons? && ValidPath(ch.head, tail); // From the definition of LowerThan(t.children, h), we get the following: match t.children { case Nil => ValidPath_Lemma(p); assert false; // absurd case case Cons(_, _) => - assert 1 <= h; + // assert 1 <= h; LowerThan_Lemma(t.children, index, h); - assert LowerThan(ch, h); + // assert LowerThan(ch, h); } // Putting these together, by ch.Cons? and the definition of LowerThan(ch, h), we get: - assert LowerThan(ch.head.children, h-1); + // assert LowerThan(ch.head.children, h-1); // And now we can invoke the induction hypothesis: - Proposition3b_Lemma(ch.head, h-1, tail); + // Proposition3b_Lemma(ch.head, h-1, tail); } } @@ -627,30 +627,10 @@ colemma Path_Lemma2'(p: Stream) } } colemma Path_Lemma2''(p: Stream, n: nat, tail: Stream) - requires IsNeverEndingStream(p) && p.tail == tail; - ensures InfinitePath'(S2N'(n, tail)); + requires IsNeverEndingStream(p) && p.tail == tail + ensures InfinitePath'(S2N'(n, tail)) { - if n <= 0 { - calc { - InfinitePath'#[_k](S2N'(n, tail)); - // def. S2N' - InfinitePath'#[_k](Zero(S2N(tail))); - // def. InfinitePath' - InfinitePath#[_k-1](S2N(tail)); - { Path_Lemma2'(tail); } - true; - } - } else { - calc { - InfinitePath'#[_k](S2N'(n, tail)); - // def. S2N' - InfinitePath'#[_k](Succ(S2N'(n-1, tail))); - // def. InfinitePath' - InfinitePath'#[_k-1](S2N'(n-1, tail)); - { Path_Lemma2''(p, n-1, tail); } - true; - } - } + Path_Lemma2'(tail); } lemma Path_Lemma3(r: CoOption) ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r)); -- cgit v1.2.3