From 2db858bf6e72e521b49aa0ae3a993dc943b8c875 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 20:39:02 -0700 Subject: Implement {:nowarn}, clarify some messages, and add a few tests --- .../some-proofs-only-work-without-autoTriggers.dfy | 48 ++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 Test/triggers/some-proofs-only-work-without-autoTriggers.dfy (limited to 'Test/triggers/some-proofs-only-work-without-autoTriggers.dfy') diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy new file mode 100644 index 00000000..98cea392 --- /dev/null +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy @@ -0,0 +1,48 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// The examples below work nicely with /autoTriggers:0, but break when we ass +// /autoTriggers. + +// The issue is that the axioms for sequences are missing a number of facts, +// which was not a problem before /autoTriggers and /stricterTriggers, but has +// become one. Here are examples of things that Dafny won’t prove with +// /autoTriggers (I would expect it wouldn’t with stricterTriggers either, +// though the second example is trickier than the first): + +method M(a: seq) { + if * { + // This fails; it needs the following axiom: + // axiom (forall s: Seq T :: + // { Seq#Take(s, Seq#Length(s)) } + // Seq#Take(s, Seq#Length(s)) == s); + assume forall x :: x in a ==> x > 0; + assert forall x :: x in a[..|a|] ==> x > 0; + } else if * { + // This fails; it needs the following axiom: + // axiom (forall s: Seq T, i: int :: + // { Seq#Index(s, i) } + // 0 <= i && i < Seq#Length(s) ==> + // Seq#Contains(s, Seq#Index(s, i))); + assume forall x :: x in a ==> x > 0; + assert forall i | 0 <= i < |a| :: a[i] > 0; + } else if * { + assume |a| > 3; + assume forall x | x in a[..3] :: x > 1; + // This fails, but here it's a lot harder to know what a good axiom would be. + assert forall x | x in a[..2] :: x > 1; + } +} + + +// In the first case, the Boogie version is +// +// Seq#Contains(Seq#Take(a#0, Seq#Length(a#0)), $Box(x#0_1)) ⟹ x#0_1 > 0 +// +// And of course Z3 picks $Box(x#0_1). The third case is similar. +// +// The problem is of course that knowing that x ∈ a[..2] doesn’t magically give +// you a term that matches x ∈ a[..3]. One could imagine introducing an extra +// symbol in the translation to put x and a together for triggering purposes, +// but that would have the same sort of issues as adding symbols for arithmetic +// operators. -- cgit v1.2.3 From 6398bd0f46ed66790d193a4dbcde3e2c0314b833 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 8 Feb 2016 18:58:34 -0800 Subject: Renamed identifiers for increased geopolitical appeal --- Test/dafny0/ResolutionErrors.dfy | 24 +++++++++++----------- Test/dafny0/ResolutionErrors.dfy.expect | 6 +++--- .../some-proofs-only-work-without-autoTriggers.dfy | 2 +- 3 files changed, 16 insertions(+), 16 deletions(-) (limited to 'Test/triggers/some-proofs-only-work-without-autoTriggers.dfy') diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 58ba6701..8dceb6ba 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -459,7 +459,7 @@ module MyOwnModule { // ------------------- nameless constructors ------------------------------ -class YHWH { +class Y { var data: int; constructor (x: int) modifies this; @@ -470,22 +470,22 @@ class YHWH { { } method Test() { - var IAmWhoIAm := new YHWH(5); - IAmWhoIAm := new YHWH._ctor(7); // but, in fact, it is also possible to use the underlying name - IAmWhoIAm := new YHWH; // error: the class has a constructor, so one must be used - var s := new Lucifer.Init(5); - s := new Lucifer.FromArray(null); - s := new Lucifer(false); - s := new Lucifer._ctor(false); - s := new Lucifer.M(); // error: there is a constructor, so one must be called - s := new Lucifer; // error: there is a constructor, so one must be called + var i := new Y(5); + i := new Y._ctor(7); // but, in fact, it is also possible to use the underlying name + i := new Y; // error: the class has a constructor, so one must be used + var s := new Luci.Init(5); + s := new Luci.FromArray(null); + s := new Luci(false); + s := new Luci._ctor(false); + s := new Luci.M(); // error: there is a constructor, so one must be called + s := new Luci; // error: there is a constructor, so one must be called var l := new Lamb; l := new Lamb(); // error: there is no default constructor l := new Lamb.Gwen(); } } -class Lucifer { +class Luci { constructor Init(y: int) { } constructor (nameless: bool) { } constructor FromArray(a: array) { } @@ -493,7 +493,7 @@ class Lucifer { } class Lamb { - method Jesus() { } + method Jess() { } method Gwen() { } } diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index b055184f..d1d826f4 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -173,9 +173,9 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David') ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1) -ResolutionErrors.dfy(475,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called -ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called -ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called +ResolutionErrors.dfy(475,6): Error: when allocating an object of type 'Y', one of its constructor methods must be called +ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called +ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int) ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy index 98cea392..bc2e0934 100644 --- a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" -// The examples below work nicely with /autoTriggers:0, but break when we ass +// The examples below work nicely with /autoTriggers:0, but break when we use // /autoTriggers. // The issue is that the axioms for sequences are missing a number of facts, -- cgit v1.2.3