Dafny:

* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks

1 files changed, 10 insertions, 0 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 1616234e..fe8644be 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -45,3 +45,13 @@ datatype ReverseOrder_TheCounterpart<T> {
   More(ReverseOrder_MutuallyRecursiveDataType<T>);

 }

 

+// ---------------------

+

+class ArrayTests {

+  ghost method G(a: array<int>)

+    requires a != null && 10 <= |a|;

+    modifies a;

+  {

+    a[7] := 13;  // error: array elements are not ghost locations

+  }

+}