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/dafny0/InductivePredicates.dfy | 41 ++++---- Test/dafny0/InductivePredicates.dfy.expect | 6 +- Test/dafny0/Parallel.dfy | 146 ++++++++++++++--------------- 3 files changed, 101 insertions(+), 92 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy index 424118e7..8d05af11 100644 --- a/Test/dafny0/InductivePredicates.dfy +++ b/Test/dafny0/InductivePredicates.dfy @@ -18,7 +18,7 @@ lemma M(x: natinf) } // yay! my first proof involving an inductive predicate :) -lemma M'(k: nat, x: natinf) +lemma {:induction false} M'(k: nat, x: natinf) requires Even#[k](x) ensures x.N? && x.n % 2 == 0 { @@ -32,8 +32,14 @@ lemma M'(k: nat, x: natinf) } } +lemma M'_auto(k: nat, x: natinf) + requires Even#[k](x) + ensures x.N? && x.n % 2 == 0 +{ +} + // Here is the same proof as in M / M', but packaged into a single "inductive lemma": -inductive lemma IL(x: natinf) +inductive lemma {:induction false} IL(x: natinf) requires Even(x) ensures x.N? && x.n % 2 == 0 { @@ -45,7 +51,7 @@ inductive lemma IL(x: natinf) } } -inductive lemma IL_EvenBetter(x: natinf) +inductive lemma {:induction false} IL_EvenBetter(x: natinf) requires Even(x) ensures x.N? && x.n % 2 == 0 { @@ -57,6 +63,12 @@ inductive lemma IL_EvenBetter(x: natinf) } } +inductive lemma IL_Best(x: natinf) + requires Even(x) + ensures x.N? && x.n % 2 == 0 +{ +} + inductive lemma IL_Bad(x: natinf) requires Even(x) ensures x.N? && x.n % 2 == 0 @@ -107,7 +119,7 @@ module Alt { { match x case N(n) => N(n+1) - case Inf => Inf + case Inf => Inf } inductive predicate Even(x: natinf) @@ -116,7 +128,7 @@ module Alt { exists y :: x == S(S(y)) && Even(y) } - inductive lemma MyLemma_NotSoNice(x: natinf) + inductive lemma {:induction false} MyLemma_NotSoNice(x: natinf) requires Even(x) ensures x.N? && x.n % 2 == 0 { @@ -130,7 +142,7 @@ module Alt { } } - inductive lemma MyLemma_NiceButNotFast(x: natinf) + inductive lemma {:induction false} MyLemma_NiceButNotFast(x: natinf) requires Even(x) ensures x.N? && x.n % 2 == 0 { @@ -143,7 +155,13 @@ module Alt { assert x.n == y.n + 2; } } - + + inductive lemma MyLemma_RealNice_AndFastToo(x: natinf) + requires Even(x) + ensures x.N? && x.n % 2 == 0 + { + } + lemma InfNotEven() ensures !Even(Inf) { @@ -156,15 +174,6 @@ module Alt { requires Even(Inf) ensures false { - var x := Inf; - if { - case x.N? && x.n == 0 => - assert false; // this case is absurd - case exists y :: x == S(S(y)) && Even(y) => - var y :| x == S(S(y)) && Even(y); - assert y == Inf; - InfNotEven_Aux(); - } } lemma NextEven(x: natinf) diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect index ccf30643..48beade5 100644 --- a/Test/dafny0/InductivePredicates.dfy.expect +++ b/Test/dafny0/InductivePredicates.dfy.expect @@ -1,9 +1,9 @@ -InductivePredicates.dfy(64,9): Error: assertion violation +InductivePredicates.dfy(76,9): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then -InductivePredicates.dfy(76,10): Error: assertion violation +InductivePredicates.dfy(88,10): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 29 verified, 2 errors +Dafny program verifier finished with 35 verified, 2 errors diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 030eb350..e0d6491b 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -2,13 +2,13 @@ // RUN: %diff "%s.expect" "%t" class C { - var data: int; - var n: nat; - var st: set; + var data: int + var n: nat + var st: set ghost method CLemma(k: int) - requires k != -23; - ensures data < k; // magic, isn't it (or bogus, some would say) + requires k != -23 + ensures data < k // magic, isn't it (or bogus, some would say) } // This method more or less just tests the syntax, resolution, and basic verification @@ -19,31 +19,31 @@ method ParallelStatement_Resolve( S: set, clx: C, cly: C, clk: int ) - requires a != null && null !in spine; - modifies a, spine; + requires a != null && null !in spine + modifies a, spine { - forall (i: int | 0 <= i < a.Length && i % 2 == 0) { + forall i | 0 <= i < a.Length && i % 2 == 0 { a[i] := a[(i + 1) % a.Length] + 3; } - forall (o | o in spine) { + forall o | o in spine { o.st := o.st + Repr; } - forall (x, y | x in S && 0 <= y+x < 100) { + forall x, y | x in S && 0 <= y+x < 100 { Lemma(clx, x, y); // error: precondition does not hold (clx may be null) } - forall (x, y | x in S && 0 <= y+x < 100) { + forall x, y | x in S && 0 <= y+x < 100 { cly.CLemma(x + y); // error: receiver might be null } - forall (p | 0 <= p) - ensures F(p) <= Sum(p) + p - 1; // error (no connection is known between F and Sum) + forall p | 0 <= p + ensures F(p) <= Sum(p) + p - 1 // error (no connection is known between F and Sum) { assert 0 <= G(p); ghost var t; - if (p % 2 == 0) { + if p % 2 == 0 { assert G(p) == F(p+2); // error (there's nothing that gives any relation between F and G) t := p+p; } else { @@ -56,11 +56,11 @@ method ParallelStatement_Resolve( } } -ghost method Lemma(c: C, x: int, y: int) - requires c != null; - ensures c.data <= x+y; -ghost method PowerLemma(x: int, y: int) - ensures Pred(x, y); +lemma Lemma(c: C, x: int, y: int) + requires c != null + ensures c.data <= x+y +lemma PowerLemma(x: int, y: int) + ensures Pred(x, y) function F(x: int): int function G(x: int): nat @@ -71,54 +71,54 @@ function Pred(x: int, y: int): bool // --------------------------------------------------------------------- method M0(S: set) - requires null !in S; - modifies S; - ensures forall o :: o in S ==> o.data == 85; - ensures forall o :: o != null && o !in S ==> o.data == old(o.data); + requires null !in S + modifies S + ensures forall o :: o in S ==> o.data == 85 + ensures forall o :: o != null && o !in S ==> o.data == old(o.data) { - forall (s | s in S) { + forall s | s in S { s.data := 85; } } method M1(S: set, x: C) - requires null !in S && x in S; + requires null !in S && x in S { - forall (s | s in S) - ensures s.data < 100; + forall s | s in S + ensures s.data < 100 { assume s.data == 85; } - if (*) { + if * { assert x.data == 85; // error (cannot be inferred from forall ensures clause) } else { assert x.data < 120; } - forall (s | s in S) - ensures s.data < 70; // error + forall s | s in S + ensures s.data < 70 // error { assume s.data == 85; } } method M2() returns (a: array) - ensures a != null; - ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j]; + ensures a != null + ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j] { a := new int[250]; - forall (i: nat | i < 125) { + forall i: nat | i < 125 { a[i] := 423; } - forall (i | 125 <= i < 250) { + forall i | 125 <= i < 250 { a[i] := 300 + i; } } method M4(S: set, k: int) - modifies S; + modifies S { - forall (s | s in S && s != null) { + forall s | s in S && s != null { s.n := k; // error: k might be negative } } @@ -127,25 +127,25 @@ method M5() { if { case true => - forall (x | 0 <= x < 100) { + forall x | 0 <= x < 100 { PowerLemma(x, x); } assert Pred(34, 34); case true => - forall (x,y | 0 <= x < 100 && y == x+1) { + forall x,y | 0 <= x < 100 && y == x+1 { PowerLemma(x, y); } assert Pred(34, 35); case true => - forall (x,y | 0 <= x < y < 100) { + forall x,y | 0 <= x < y < 100 { PowerLemma(x, y); } assert Pred(34, 35); case true => - forall (x | x in set k | 0 <= k < 100) { + forall x | x in set k | 0 <= k < 100 { PowerLemma(x, x); } assert Pred(34, 34); @@ -155,22 +155,22 @@ method M5() method Main() { var a := new int[180]; - forall (i | 0 <= i < 180) { + forall i | 0 <= i < 180 { a[i] := 2*i + 100; } var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5]; - forall (i | 0 <= i < |sq|) { + forall i | 0 <= i < |sq| { a[20+i] := sq[i]; } - forall (t | t in sq) { + forall t | t in sq { a[t] := 1000; } - forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) { + forall t,u | t in sq && t < 4 && 10 <= u < 10+t { a[u] := 6000 + t; } var k := 0; - while (k < 180) { - if (k != 0) { print ", "; } + while k < 180 { + if k != 0 { print ", "; } print a[k]; k := k + 1; } @@ -180,50 +180,50 @@ method Main() method DuplicateUpdate() { var a := new int[180]; var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5]; - if (*) { - forall (t,u | t in sq && 10 <= u < 10+t) { + if * { + forall t,u | t in sq && 10 <= u < 10+t { a[u] := 6000 + t; // error: a[10] (and a[11]) are assigned more than once } } else { - forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) { + forall t,u | t in sq && t < 4 && 10 <= u < 10+t { a[u] := 6000 + t; // with the 't < 4' conjunct in the line above, this is fine } } } -ghost method DontDoMuch(x: int) +lemma DontDoMuch(x: int) { } method OmittedRange() { - forall (x: int) { } // a type is still needed for the bound variable - forall (x) { + forall x: int { } // a type is still needed for the bound variable + forall x { DontDoMuch(x); } } // ----------------------- two-state postconditions --------------------------------- -class TwoState_C { ghost var data: int; } +class TwoState_C { ghost var data: int } // It is not possible to achieve this postcondition in a ghost method, because ghost // contexts are not allowed to allocate state. Callers of this ghost method will know // that the postcondition is tantamount to 'false'. ghost method TwoState0(y: int) - ensures exists o: TwoState_C :: o != null && fresh(o); + ensures exists o: TwoState_C :: o != null && fresh(o) method TwoState_Main0() { - forall (x) { TwoState0(x); } + forall x { TwoState0(x); } assert false; // no prob, because the postcondition of TwoState0 implies false } method X_Legit(c: TwoState_C) - requires c != null; - modifies c; + requires c != null + modifies c { c.data := c.data + 1; - forall (x | c.data <= x) - ensures old(c.data) < x; // note that the 'old' refers to the method's initial state + forall x | c.data <= x + ensures old(c.data) < x // note that the 'old' refers to the method's initial state { } } @@ -235,8 +235,8 @@ method X_Legit(c: TwoState_C) // method, not the beginning of the 'forall' statement. method TwoState_Main2() { - forall (x: int) - ensures exists o: TwoState_C :: o != null && fresh(o); + forall x: int + ensures exists o: TwoState_C :: o != null && fresh(o) { TwoState0(x); } @@ -251,8 +251,8 @@ method TwoState_Main2() // statement's effect on the heap is not optimized away. method TwoState_Main3() { - forall (x: int) - ensures exists o: TwoState_C :: o != null && fresh(o); + forall x: int + ensures exists o: TwoState_C :: o != null && fresh(o) { assume false; // (there's no other way to achieve this forall-statement postcondition) } @@ -262,11 +262,11 @@ method TwoState_Main3() // ------- empty forall statement ----------------------------------------- class EmptyForallStatement { - var emptyPar: int; + var emptyPar: int method Empty_Parallel0() - modifies this; - ensures emptyPar == 8; + modifies this + ensures emptyPar == 8 { forall () { this.emptyPar := 8; @@ -274,11 +274,11 @@ class EmptyForallStatement { } function EmptyPar_P(x: int): bool - ghost method EmptyPar_Lemma(x: int) - ensures EmptyPar_P(x); + lemma EmptyPar_Lemma(x: int) + ensures EmptyPar_P(x) method Empty_Parallel1() - ensures EmptyPar_P(8); + ensures EmptyPar_P(8) { forall { EmptyPar_Lemma(8); @@ -288,7 +288,7 @@ class EmptyForallStatement { method Empty_Parallel2() { forall - ensures exists k :: EmptyPar_P(k); + ensures exists k :: EmptyPar_P(k) { var y := 8; assume EmptyPar_P(y); @@ -312,9 +312,9 @@ predicate ThProperty(step: nat, t: Nat, r: nat) case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro) } -ghost method Th(step: nat, t: Nat, r: nat) - requires t.Succ? && ThProperty(step, t, r); +lemma Th(step: nat, t: Nat, r: nat) + requires t.Succ? && ThProperty(step, t, r) // the next line follows from the precondition and the definition of ThProperty - ensures exists ro:nat :: ThProperty(step-1, t.tail, ro); + ensures exists ro:nat :: ThProperty(step-1, t.tail, ro) { } -- cgit v1.2.3