diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:07:59 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:07:59 -0700 |
| commit | 37bd956ddccbb0ccaa1f30a1283a2932178555d2 (patch) | |
| tree | 4e4071f436870ed590980c56fed75381cf3db81f /Binaries | |
| parent | 6044f08dceb6c03e7b6e8924186a301dcc2e7e97 (diff) | |
Added some axioms to try to recover boxed data. In particular, any element 'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 8ca70bac..a605ba87 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -434,6 +434,15 @@ function $IsCanonicalBoolBox(BoxType): bool; axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));
axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);
+// The following function and axiom are used to obtain a $Box($Unbox(_)) wrapper around
+// certain expressions. Note that it assumes any booleans contained in the set are canonical
+// (which is the case for any set that occurs in an execution of a Dafny program).
+// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction
+// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'.
+function $IsGoodSet<T>(s: Set BoxType, dummy: T): bool;
+axiom (forall<T> ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet(ss, dummy), ss[bx] }
+ $IsGoodSet(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx):T));
+
// ---------------------------------------------------------------
// -- Encoding of type names -------------------------------------
// ---------------------------------------------------------------
|