From 37bd956ddccbb0ccaa1f30a1283a2932178555d2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 17 Oct 2012 14:07:59 -0700 Subject: 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. --- Binaries/DafnyPrelude.bpl | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'Binaries') 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(s: Set BoxType, dummy: T): bool; +axiom (forall 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 ------------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3