From a93abfeb96437977f2cbd56c0e99610af6f12386 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 2 Apr 2014 18:59:29 -0700
Subject: Improvements in sequence axioms to make checking more automatic.
 Minor changes in a test file.

---
 Test/dafny3/GenericSort.dfy | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 5ae512de..10589e5a 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -1,4 +1,4 @@
-module TotalOrder {
+abstract module TotalOrder {
   type T // the type to be compared
   static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
   // Three properties of total orders.  Here, they are given as unproved
@@ -13,7 +13,7 @@ module TotalOrder {
     ensures Leq(a, b) || Leq(b, a);
 }
 
-module Sort {
+abstract module Sort {
   import O as TotalOrder  // let O denote some module that has the members of TotalOrder
 
   static predicate Sorted(a: array<O.T>, low: int, high: int)
@@ -141,5 +141,7 @@ module Client {
      assert IntSort.O.Leq(a[1], a[2]);  // lemma
      assert IntSort.O.Leq(a[2], a[3]);  // lemma
      assert a[..] == [I.T.Int(0), I.T.Int(1), I.T.Int(4), I.T.Int(6)];
+     // why not print out the result!
+     print a[..], "\n";
   }
 }
-- 
cgit v1.2.3