diff options
| author |  rustanleino <unknown> | 2009-11-06 22:00:56 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-06 22:00:56 +0000 |
| commit | 660c22dc282ee371fdbd4c97e9289ee016a4aca8 (patch) | |
| tree | bcb6b2c773afbe0e6ee732f0cf6fcbf7964ba3d2 /Binaries | |
| parent | 43004594801ab135fde6dbd69a38521a95a30f70 (diff) | |
Redesigned the encoding of Dafny generics, including the built-in types set and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 75c5777e..9615586a 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -148,10 +148,17 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } // -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
-function $Box<T>(T) returns (ref);
-function $Unbox<T>(ref) returns (T);
+type BoxType;
+
+function $Box<T>(T) returns (BoxType);
+function $Unbox<T>(BoxType) returns (T);
axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
+axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
+axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
+axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
+// note: an axiom like this for bool would not be sound
// ---------------------------------------------------------------
|