Merge

4 files changed, 124 insertions, 1 deletions

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 02335678..65db7f7f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -715,3 +715,98 @@ class GT {
     }

   }

 }

+

+// ----- tests of various ways to express that a collection is nonempty, showing that these all lead to being

+// ----- able to pick an element from the (domain of the) collection

+

+module GenericPick {

+  function SetPick0<U>(s: set<U>): U

+    requires s != {}

+  {

+    var x :| x in s; x

+  }

+  function SetPick1<U>(s: set<U>): U

+    requires |s| != 0

+  {

+    var x :| x in s; x

+  }

+  function SetPick2<U>(s: set<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+

+  function MultisetPick0<U>(s: multiset<U>): U

+    requires s != multiset{}

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick1<U>(s: multiset<U>): U

+    requires |s| != 0

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick2<U>(s: multiset<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick3<U>(s: multiset<U>): U

+    requires exists x :: s[x] > 0

+  {

+    var x :| x in s; x

+  }

+

+  function SeqPick0<U>(s: seq<U>): U

+    requires s != []

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick1<U>(s: seq<U>): U

+    requires |s| != 0

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick2<U>(s: seq<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+  function SeqPick3<U>(s: seq<U>): U

+    requires exists i :: 0 <= i < |s|

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick4<U>(s: seq<U>): U

+    requires exists i :: 0 <= i < |s|

+  {

+    var i :| 0 <= i < |s|; s[i]

+  }

+  lemma EquivalentWaysOfSayingSequenceIsNonempty<U>(s: seq<U>)

+    requires s != []

+          || |s| != 0

+          || exists i :: 0 <= i < |s|

+    ensures exists x :: x in s

+  {

+    assert s[0] in s;

+  }

+

+  function MapPick0<U,V>(m: map<U,V>): U

+    requires m != map[]

+  {

+    var x :| x in m; x

+  }

+  function MapPick1<U,V>(m: map<U,V>): U

+    requires |m| != 0

+  {

+    var x :| x in m; x

+  }

+  function MapPick2<U,V>(m: map<U,V>): U

+    requires exists x :: x in m

+  {

+    var x :| x in m; x

+  }

+}

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 1983d2ac..5f766cd6 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -196,6 +196,6 @@ SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 87 verified, 35 errors

+Dafny program verifier finished with 104 verified, 35 errors

 

 Dafny program verifier finished with 0 verified, 0 errors

diff --git a/Test/dafny4/Bug54.dfy b/Test/dafny4/Bug54.dfy
new file mode 100644
index 00000000..c975ec9a
--- /dev/null
+++ b/Test/dafny4/Bug54.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+predicate G<X>(f:X->bool)

+  reads f.reads;

+  requires forall x :: f.requires(x) && f(x);

+{

+  true

+}

+

+predicate H()

+{

+  G((x:int) => true)

+}

+

+predicate P1<X>(m:map<X,bool>)

+  requires forall x :: x in m ==> m[x];

+{

+  true

+}

+

+predicate P2(m:map<int,bool>)

+  requires forall x :: x in m ==> m[x];

+{

+  P1(map x:int | x in m :: true)

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug54.dfy.expect b/Test/dafny4/Bug54.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny4/Bug54.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors