From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Binaries/DafnyPrelude.bpl | 91 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 91 insertions(+) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 74bdb63e..5ee8b845 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -20,6 +20,7 @@ const unique TInt : Ty; const unique TNat : Ty; const unique TReal : Ty; function TSet(Ty) : Ty; +function TISet(Ty) : Ty; function TMultiSet(Ty) : Ty; function TSeq(Ty) : Ty; function TMap(Ty, Ty) : Ty; @@ -27,6 +28,8 @@ function TIMap(Ty, Ty) : Ty; function Inv0_TSet(Ty) : Ty; axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); +function Inv0_TISet(Ty) : Ty; +axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t); function Inv0_TSeq(Ty) : Ty; axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t); function Inv0_TMultiSet(Ty) : Ty; @@ -52,6 +55,7 @@ const unique TagInt : TyTag; const unique TagNat : TyTag; const unique TagReal : TyTag; const unique TagSet : TyTag; +const unique TagISet : TyTag; const unique TagMultiSet : TyTag; const unique TagSeq : TyTag; const unique TagMap : TyTag; @@ -64,6 +68,7 @@ axiom Tag(TInt) == TagInt; axiom Tag(TNat) == TagNat; axiom Tag(TReal) == TagReal; axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet); +axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet); axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap); @@ -137,6 +142,9 @@ axiom (forall bx : Box :: axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TSet(t)) } ( $IsBox(bx, TSet(t)) ==> $Box($Unbox(bx) : Set Box) == bx && $Is($Unbox(bx) : Set Box, TSet(t)))); +axiom (forall bx : Box, t : Ty :: + { $IsBox(bx, TISet(t)) } + ( $IsBox(bx, TISet(t)) ==> $Box($Unbox(bx) : ISet Box) == bx && $Is($Unbox(bx) : ISet Box, TISet(t)))); axiom (forall bx : Box, t : Ty :: { $IsBox(bx, TMultiSet(t)) } ( $IsBox(bx, TMultiSet(t)) ==> $Box($Unbox(bx) : MultiSet Box) == bx && $Is($Unbox(bx) : MultiSet Box, TMultiSet(t)))); @@ -187,6 +195,10 @@ axiom (forall v: Set Box, t0: Ty :: { $Is(v, TSet(t0)) } $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0))); +axiom (forall v: ISet Box, t0: Ty :: { $Is(v, TISet(t0)) } + $Is(v, TISet(t0)) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsBox(bx, t0))); axiom (forall v: MultiSet Box, t0: Ty :: { $Is(v, TMultiSet(t0)) } $Is(v, TMultiSet(t0)) <==> (forall bx: Box :: { v[bx] } @@ -202,6 +214,10 @@ axiom (forall v: Set Box, t0: Ty, h: Heap :: { $IsAlloc(v, TSet(t0), h) } $IsAlloc(v, TSet(t0), h) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h))); +axiom (forall v: ISet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TISet(t0), h) } + $IsAlloc(v, TISet(t0), h) <==> + (forall bx: Box :: { v[bx] } + v[bx] ==> $IsAllocBox(bx, t0, h))); axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: { $IsAlloc(v, TMultiSet(t0), h) } $IsAlloc(v, TMultiSet(t0), h) <==> (forall bx: Box :: { v[bx] } @@ -544,6 +560,81 @@ function Set#Disjoint(Set T, Set T): bool; axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); +// --------------------------------------------------------------- +// -- Axiomatization of isets ------------------------------------- +// --------------------------------------------------------------- + +type ISet T = [T]bool; + +function ISet#Empty(): Set T; +axiom (forall o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(ISet#Empty() : [T]bool, TISet(t)) } $Is(ISet#Empty() : [T]bool, TISet(t))); + + +function ISet#UnionOne(ISet T, T): ISet T; +axiom (forall a: ISet T, x: T, o: T :: { ISet#UnionOne(a,x)[o] } + ISet#UnionOne(a,x)[o] <==> o == x || a[o]); +axiom (forall a: ISet T, x: T :: { ISet#UnionOne(a, x) } + ISet#UnionOne(a, x)[x]); +axiom (forall a: ISet T, x: T, y: T :: { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Union(a,b)[o] } + ISet#Union(a,b)[o] <==> a[o] || b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: Set T, y: T :: { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); +axiom (forall a, b: ISet T :: { ISet#Union(a, b) } + ISet#Disjoint(a, b) ==> + ISet#Difference(ISet#Union(a, b), a) == b && + ISet#Difference(ISet#Union(a, b), b) == a); +// Follows from the general union axiom, but might be still worth including, because disjoint union is a common case: +// axiom (forall a, b: ISet T :: { ISet#Card(ISet#Union(a, b)) } +// ISet#Disjoint(a, b) ==> +// ISet#Card(ISet#Union(a, b)) == ISet#Card(a) + ISet#Card(b)); + +function ISet#Intersection(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Intersection(a,b)[o] } + ISet#Intersection(a,b)[o] <==> a[o] && b[o]); + +axiom (forall a, b: ISet T :: { ISet#Union(ISet#Union(a, b), b) } + ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b)); +axiom (forall a, b: Set T :: { ISet#Union(a, ISet#Union(a, b)) } + ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(ISet#Intersection(a, b), b) } + ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b)); +axiom (forall a, b: ISet T :: { ISet#Intersection(a, ISet#Intersection(a, b)) } + ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b)); + + +function ISet#Difference(ISet T, ISet T): ISet T; +axiom (forall a: ISet T, b: ISet T, o: T :: { ISet#Difference(a,b)[o] } + ISet#Difference(a,b)[o] <==> a[o] && !b[o]); +axiom (forall a, b: ISet T, y: T :: { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y] ); + +function ISet#Subset(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Subset(a,b) } + ISet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); +// axiom(forall a: ISet T, b: ISet T :: +// { ISet#Subset(a,b), ISet#Card(a), ISet#Card(b) } // very restrictive trigger +// ISet#Subset(a,b) ==> ISet#Card(a) <= ISet#Card(b)); + + +function ISet#Equal(ISet T, ISet T): bool; +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } + ISet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); +axiom(forall a: ISet T, b: ISet T :: { ISet#Equal(a,b) } // extensionality axiom for sets + ISet#Equal(a,b) ==> a == b); + +function ISet#Disjoint(ISet T, ISet T): bool; +axiom (forall a: ISet T, b: ISet T :: { ISet#Disjoint(a,b) } + ISet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); + // --------------------------------------------------------------- // -- Axiomatization of multisets -------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3 From dd8117ebb70bdb1531a35eb47f490929a5c658fb Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 7 Jun 2015 11:49:47 -0700 Subject: Fix the Seq#Contain axiom; it should talk about T, not ref. --- Binaries/DafnyPrelude.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 5ee8b845..ef6106e0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -836,7 +836,7 @@ function Seq#Contains(Seq T, T): bool; axiom (forall s: Seq T, x: T :: { Seq#Contains(s,x) } Seq#Contains(s,x) <==> (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x)); -axiom (forall x: ref :: +axiom (forall x: T :: { Seq#Contains(Seq#Empty(), x) } !Seq#Contains(Seq#Empty(), x)); -- cgit v1.2.3 From 91fa6b7d576a111f39cde20de5d8e612b4d712b5 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 25 Jun 2015 18:12:53 -0700 Subject: Tried to reduce frame-axiom instantiations by saying the earlier heap must be a "heap anchor". Currently, a heap is an anchor if it produced by a havoc (but not a direct update). --- Binaries/DafnyPrelude.bpl | 3 ++- Source/Dafny/Translator.cs | 29 +++++++++++++++++++---------- Test/VSI-Benchmarks/b3.dfy | 10 ++++++++-- Test/VerifyThis2015/Problem3.dfy | 2 +- 4 files changed, 30 insertions(+), 14 deletions(-) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ef6106e0..dbf9b76c 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -398,7 +398,8 @@ function {:inline true} read(H:Heap, r:ref, f:Field alpha): alpha { H[r, function {:inline true} update(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r,f := v] } function $IsGoodHeap(Heap): bool; -var $Heap: Heap where $IsGoodHeap($Heap); +function $IsHeapAnchor(Heap): bool; +var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap); function $HeapSucc(Heap, Heap): bool; axiom (forall h: Heap, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 90d0b11c..4324b2b8 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1761,7 +1761,7 @@ namespace Microsoft.Dafny { var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType); Bpl.Expr wh = BplAnd( FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, oih), - FunctionCall(iter.tok, BuiltinFunction.HeapSucc, null, oih, etran.HeapExpr)); + HeapSucc(oih, etran.HeapExpr)); localVariables.Add(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh))); // do an initial YieldHavoc @@ -3692,9 +3692,9 @@ namespace Microsoft.Dafny { /// /// Generates: /// axiom (forall s, h0: HeapType, h1: HeapType, formals... :: - /// { HeapSucc(h0,h1), F(s,h1,formals) } + /// { IsHeapAnchor(h0), HeapSucc(h0,h1), F(s,h1,formals) } /// heaps are well-formed and formals are allocated AND - /// HeapSucc(h0,h1) + /// IsHeapAnchor(h0) AND HeapSucc(h0,h1) /// AND /// (forall(alpha) o: ref, f: Field alpha :: /// o != null AND h0[o,alloc] AND h1[o,alloc] AND @@ -3813,7 +3813,8 @@ namespace Microsoft.Dafny { Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o))); Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field)); - Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1); + Bpl.Expr h0IsHeapAnchor = FunctionCall(h0.tok, BuiltinFunction.IsHeapAnchor, null, h0); + Bpl.Expr heapSucc = HeapSucc(h0, h1); Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null); Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new List { alpha }, new List { oVar, fieldVar }, Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged)); @@ -3873,11 +3874,11 @@ namespace Microsoft.Dafny { var F0 = new Bpl.NAryExpr(f.tok, fn, f0args); var F1 = new Bpl.NAryExpr(f.tok, fn, f1args); var eq = Bpl.Expr.Eq(F0, F1); - var tr = new Bpl.Trigger(f.tok, true, new List { heapSucc, F1 }); + var tr = new Bpl.Trigger(f.tok, true, new List { h0IsHeapAnchor, heapSucc, F1 }); var typeParams = TrTypeParamDecls(f.TypeArgs); var ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr, - Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc), + Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, Bpl.Expr.And(h0IsHeapAnchor, heapSucc)), Bpl.Expr.Imp(q0, eq))); sink.AddTopLevelDeclaration(new Bpl.Axiom(f.tok, ax, comment)); #endif @@ -5829,7 +5830,7 @@ namespace Microsoft.Dafny { var h0 = BplBoundVar("h0", predef.HeapType, bvars); var h1 = BplBoundVar("h1", predef.HeapType, bvars); - var heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, h0, h1); + var heapSucc = HeapSucc(h0, h1); var goodHeaps = BplAnd( FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h0), FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h1)); @@ -6683,7 +6684,7 @@ namespace Microsoft.Dafny { // the frame condition, which is free since it is checked with every heap update and call boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, isGhostContext, etranPre, etran, etranMod), null, "frame condition")); // HeapSucc(S1, S2) or HeapSuccGhost(S1, S2) - Bpl.Expr heapSucc = FunctionCall(tok, isGhostContext ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr); + Bpl.Expr heapSucc = HeapSucc(etranPre.HeapExpr, etran.HeapExpr, isGhostContext); boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate")); } return boilerplate; @@ -7316,7 +7317,7 @@ namespace Microsoft.Dafny { // havoc $Heap; builder.Add(new Bpl.HavocCmd(s.Tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); // assume $HeapSucc(preModifyHeap, $Heap); OR $HeapSuccGhost - builder.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, s.IsGhost ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, preModifyHeap, etran.HeapExpr))); + builder.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost))); // assume nothing outside the frame was changed var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap); var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName); @@ -7867,7 +7868,7 @@ namespace Microsoft.Dafny { var prevEtran = new ExpressionTranslator(this, predef, prevHeap); updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr)); updater.Add(new Bpl.HavocCmd(s.Tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); - updater.Add(new Bpl.AssumeCmd(s.Tok, FunctionCall(s.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr))); + updater.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr))); // Here comes: // assume (forall o: ref, f: Field alpha :: @@ -11913,6 +11914,7 @@ namespace Microsoft.Dafny { IntToReal, IsGoodHeap, + IsHeapAnchor, HeapSucc, HeapSuccGhost, @@ -12293,6 +12295,10 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); return FunctionCall(tok, "$IsGoodHeap", Bpl.Type.Bool, args); + case BuiltinFunction.IsHeapAnchor: + Contract.Assert(args.Length == 1); + Contract.Assert(typeInstantiation == null); + return FunctionCall(tok, "$IsHeapAnchor", Bpl.Type.Bool, args); case BuiltinFunction.HeapSucc: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); @@ -14131,6 +14137,9 @@ namespace Microsoft.Dafny { Bpl.Expr.Eq(oldHeap, newHeap), FunctionCall(newHeap.tok, BuiltinFunction.HeapSucc, null, oldHeap, newHeap)); } + Bpl.Expr HeapSucc(Bpl.Expr oldHeap, Bpl.Expr newHeap, bool useGhostHeapSucc = false) { + return FunctionCall(newHeap.tok, useGhostHeapSucc ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, oldHeap, newHeap); + } // Bpl-making-utilities diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index f59b0c3e..d47c4d4d 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -96,7 +96,7 @@ class Benchmark3 { if x < m { k := j; m := x; } j := j+1; } - + j := 0; while j < k invariant j <= k; @@ -108,10 +108,16 @@ class Benchmark3 { RotationLemma(old(q.contents), j, qc0, q.contents); j := j+1; } - + assert j == k; assert q.contents == old(q.contents)[k..] + old(q.contents)[..k]; + ghost var qq := q.contents; m := q.Dequeue(); + assert q.contents == qq[1..] && m == qq[0]; + assert [m] + q.contents == qq; + assert |old(q.contents)| == |q.contents| + 1; + + assert q.contents == old(q.contents)[k+1..] + old(q.contents)[..k]; } lemma RotationLemma(O: seq, j: nat, A: seq, C: seq) diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 4205035d..10ad2d3a 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino -- cgit v1.2.3 From 550caf7bc7e6427f26bfb3d24f224e12c6c1c318 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 1 Jul 2015 13:29:11 -0700 Subject: Fixed bug in BplImp! Improvements in encoding of reads of function values. --- Binaries/DafnyPrelude.bpl | 8 ++++++++ Source/Dafny/Translator.cs | 16 +++++++--------- Test/VerifyThis2015/Problem3.dfy | 2 +- Test/dafny4/NumberRepresentations.dfy | 2 +- 4 files changed, 17 insertions(+), 11 deletions(-) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index dbf9b76c..2ca10f73 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -273,6 +273,8 @@ const unique class._System.set: ClassName; const unique class._System.seq: ClassName; const unique class._System.multiset: ClassName; +function Tclass._System.object(): Ty; + function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty function TypeTuple(a: ClassName, b: ClassName): ClassName; @@ -287,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type HandleType; +function SetRef_to_SetBox(s: [ref]bool): Set Box; +axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] } + SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]); +axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) } + $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object()))); + // --------------------------------------------------------------- // -- Datatypes -------------------------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c98bd203..78f5c89d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5713,11 +5713,9 @@ namespace Microsoft.Dafny { { // forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box - // :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN] - // - // no precondition for these, but: - // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN] - // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't + // :: ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == h[heap, b1, ..., bN] + // :: RequiresN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) <== r[heap, b1, ..., bN] + // :: ReadsN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == rd[heap, b1, ..., bN] Action SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => { Contract.Assert((precond == null) == (precondTy == null)); var bvars = new List(); @@ -5919,7 +5917,7 @@ namespace Microsoft.Dafny { var inner_name = GetClass(td).TypedIdent.Name; string name = "T" + inner_name; // Create the type constructor - { + if (td.Name != "object") { // the type constructor for "object" is in DafnyPrelude.bpl Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false); List args = new List( Enumerable.Range(0, arity).Select(i => @@ -11462,10 +11460,10 @@ namespace Microsoft.Dafny { } var rdvars = new List(); - var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType()); - + var o = BplBoundVar(varNameGen.FreshId("#o#"), predef.RefType, rdvars); Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List(), rdvars, null, translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null)); + rdbody = translator.FunctionCall(e.tok, "SetRef_to_SetBox", predef.SetType(e.tok, true, predef.BoxType), rdbody); return translator.Lit( translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType, @@ -14220,7 +14218,7 @@ namespace Microsoft.Dafny { Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); - if (a == Bpl.Expr.True || b == Bpl.Expr.True || b == Bpl.Expr.False) { + if (a == Bpl.Expr.True || b == Bpl.Expr.True) { return b; } else if (a == Bpl.Expr.False) { return Bpl.Expr.True; diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 10ad2d3a..4205035d 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Rustan Leino diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 8a94505c..1ebdf64c 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // We consider a number representation that consists of a sequence of digits. The least -- cgit v1.2.3