From 3a87ca70392a4b8d8d5bcdd8ed921cfdfc47452c Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 29 Jun 2011 16:49:45 -0700
Subject: Dafny: Fixed axioms for Seq#Contains vs. the sequence building
 functions

---
 Binaries/DafnyPrelude.bpl  | 15 ++++++++++-----
 Test/dafny0/Answer         |  7 ++++++-
 Test/dafny0/SmallTests.dfy | 16 ++++++++++++++++
 3 files changed, 32 insertions(+), 6 deletions(-)

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 30992d46..94a8833a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -137,11 +137,16 @@ axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
   { Seq#Contains(Seq#Append(s0, s1), x) }
   Seq#Contains(Seq#Append(s0, s1), x) <==>
     Seq#Contains(s0, x) || Seq#Contains(s1, x));
-axiom (forall<T> s: Seq T, i: int, v: T, len: int, x: T ::
-  { Seq#Contains(Seq#Build(s, i, v, len), x) }
-  Seq#Contains(Seq#Build(s, i, v, len), x) <==>
-    (0 <= i && i < len && x == v)  ||  
-    (exists j: int :: { Seq#Index(s,j) } 0 <= j && j < Seq#Length(s) && j < len && j!=i && Seq#Index(s,j) == x));
+axiom (forall<T> i: int, v: T, len: int, x: T ::
+  { Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) }
+  0 <= i && i < len ==>
+  (Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) <==> x == v));
+axiom (forall<T> s: Seq T, i0: int, v0: T, len0: int, i1: int, v1: T, len1: int, x: T ::
+  { Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) }
+  0 <= i0 && i0 < len0 && len0 <= i1 && i1 < len1 ==>
+  (Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) <==>
+     v1 == x ||
+     Seq#Contains(Seq#Build(s, i0, v0, len0), x)));
 axiom (forall<T> s: Seq T, n: int, x: T ::
   { Seq#Contains(Seq#Take(s, n), x) }
   Seq#Contains(Seq#Take(s, n), x) <==>
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 29b8e708..e20f2253 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -200,8 +200,13 @@ Execution trace:
     (0,0): anon24_Then
     (0,0): anon15
     (0,0): anon25_Else
+SmallTests.dfy(347,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Then
+    (0,0): anon7
 
-Dafny program verifier finished with 43 verified, 14 errors
+Dafny program verifier finished with 44 verified, 15 errors
 
 -------------------- Definedness.dfy --------------------
 Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index ac7286e9..8393b1c7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -330,3 +330,19 @@ class SomeType
     }
   }
 }
+
+// ----------------------- tests of some theory axioms --------
+
+method TestSequences0()
+{
+  var s := [0, 2, 4];
+  if (*) {
+    assert 4 in s;
+    assert 0 in s;
+    assert 1 !in s;
+  } else {
+    assert 2 in s;
+    assert exists n :: n in s && -3 <= n && n < 2;
+  }
+  assert 7 in s;  // error
+}
-- 
cgit v1.2.3