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

1 files changed, 0 insertions, 4 deletions

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);