Dafny: Since it's no longer true that all types support equality at run-time (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.

8 files changed, 16 insertions, 12 deletions

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b70ff4d0..76e1ffa7 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -14,7 +14,7 @@
 // that the specification can use mathematical sequences while the

 // implementation uses a linked list.

 

-class Map<Key,Value> {

+class Map<Key(==),Value> {

   ghost var Keys: seq<Key>;

   ghost var Values: seq<Value>;

   ghost var Repr: set<object>;

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 383bccfd..2149df25 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -250,7 +250,7 @@ class WriterStream {
   

   

   

-class Map<Key,Value> {

+class Map<Key(==),Value> {

   var keys: seq<Key>;

   var values: seq<Value>;

   

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index e8b618d7..40df1135 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
   assert x != y;

 }

 

-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)

+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)

   requires 0 <= N && N <= |a|;

   requires exists k | 0 <= k && k < N :: a[k] == y;

   ensures forall k | 0 <= k && k < N :: a[k] == y;  // error

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index d6804661..cb9b5660 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -1,11 +1,11 @@
-class C<U> {

+class C<U(==)> {

   method M<T>(x: T, u: U) returns (y: T)

     ensures x == y && u == u;

   {

     y := x;

   }

 

-  function method F<X>(x: X, u: U): bool

+  function method F<X(==)>(x: X, u: U): bool

   {

     x == x && u == u

   }

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..4c761671 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
 }

 

 method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

-  requires (exists c :: IsCelebrity(c, people));

+  requires exists c :: IsCelebrity(c, people);

   ensures r == c;

 {

   var cc; assume cc == c;  // this line essentially converts ghost c to non-ghost cc

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..c78d5e81 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,6 +1,6 @@
 // ultra filter

 

-class UltraFilter<G> {

+class UltraFilter<G(==)> {

   static function IsFilter(f: set<set<G>>, S: set<G>): bool

   {

     (forall A, B :: A in f && A <= B ==> B in f) &&

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index a7512486..af67ee92 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -31,6 +31,10 @@
 // choice, if there is such a choice, and then passes in that choice as the ghost parameter K

 // to the main algorithm.  Neat, huh?

 

+// Language comment:

+// The "(==)" that sits after some type parameters in this program says that the actual

+// type argument must support equality.

+

 // Advanced remark:

 // There is a subtle situation in the verification of DetermineElection.  Suppose the type

 // parameter Candidate denotes some type whose instances depend on which object are

@@ -47,7 +51,7 @@
 // to the Count function.  Alternatively, one could have added the antecedent "c in a" or

 // "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.

 

-function method Count<T>(a: seq<T>, s: int, t: int, x: T): int

+function method Count<T(==)>(a: seq<T>, s: int, t: int, x: T): int

   requires 0 <= s <= t <= |a|;

   ensures Count(a, s, t, x) == 0 || x in a;

 {

@@ -57,7 +61,7 @@ function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
 

 // Here is the first version of the algorithm, the one that assumes there is a majority choice.

 

-method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

+method FindWinner<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

   requires 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

   ensures k == K;  // find K

 {

@@ -93,7 +97,7 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k:
 // Here is the second version of the program, the one that also computes whether or not

 // there is a majority choice.

 

-method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

+method DetermineElection<Candidate(==)>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

   ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;

   ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;

 {

@@ -107,7 +111,7 @@ method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool,
 // antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"

 // statement.

 

-method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

+method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

   requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

   ensures hasWinner ==> k == K;  // find K

 {

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index 5153b053..4373136b 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -1,4 +1,4 @@
-class BreadthFirstSearch<Vertex>

+class BreadthFirstSearch<Vertex(==)>

 {

   // The following function is left uninterpreted (for the purpose of the 

   // verification problem, it can be thought of as a parameter to the class)