summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-21 19:16:05 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-21 19:16:05 -0700
commitb0d1f6cc6a6d4f0ea1c64ae6de053061f4697375 (patch)
treef8bba784923413c213a6085125beb5baf5dbc13b /Test/VSI-Benchmarks
parentfbb49d063841042511bf29c48892ef82e42853a1 (diff)
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.
Diffstat (limited to 'Test/VSI-Benchmarks')
-rw-r--r--Test/VSI-Benchmarks/b4.dfy2
-rw-r--r--Test/VSI-Benchmarks/b8.dfy2
2 files changed, 2 insertions, 2 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>;