From 4744c729d2fa83f324ffa84dc619ad0a321a9c98 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 17 Sep 2010 01:26:47 +0000
Subject: Dafny: * Added full support for multi-dimensional arrays (except for
 one issue that still needs to be added in compilation) * Changed syntax of
 array length from |a| to a.Length (for one-dimensional arrays).  The syntax
 for either dimensions is, for example, b.Length0 and b.Length1 for
 2-dimensional arrays. * Internally, this meant adding support for built-in
 classes and readonly fields

---
 Binaries/DafnyPrelude.bpl | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ad4dcbae..476a6bd9 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -207,7 +207,6 @@ axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): Datatype
 type ClassName;
 const unique class.int: ClassName;
 const unique class.bool: ClassName;
-const unique class.object: ClassName;
 const unique class.set: ClassName;
 const unique class.seq: ClassName;
 
@@ -273,9 +272,6 @@ function DeclType<T>(Field T) returns (ClassName);
 // -- Arrays -----------------------------------------------------
 // ---------------------------------------------------------------
 
-function Array#Length(ref, int): int;
-axiom (forall r: ref, dim: int :: 0 <= Array#Length(r, dim));
-
 procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
   modifies $Heap;
   ensures $HeapSucc(old($Heap), $Heap);
-- 
cgit v1.2.3