From 8718c8de05f07ffbb3ccbceee550a9c88a599947 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 6 Nov 2009 23:54:22 +0000
Subject: Added a sequence update expression in Dafny.

---
 Binaries/DafnyPrelude.bpl | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 9615586a..4eee233b 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -84,6 +84,14 @@ axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Bui
     (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
     (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
 
+function Seq#Update<T>(Seq T, int, T) returns (Seq T);
+axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
+  0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
+axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }
+  0 <= n && n < Seq#Length(s) ==>
+    (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&
+    (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));
+
 function Seq#Contains<T>(Seq T, T) returns (bool);
 axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
   Seq#Contains(s,x) <==>
-- 
cgit v1.2.3