From bb6f5a2ad132f7d5553b4506f00bced4f1af3c73 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Mon, 11 Jul 2011 17:22:32 -0700 Subject: Added s[..] syntax in anticipation of sequence forming operation. (also updated regression tests.) --- Test/dafny0/Answer | 8 ++++---- Test/dafny0/Array.dfy | 3 +++ 2 files changed, 7 insertions(+), 4 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7a972f22..a6f1e9b7 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -487,20 +487,20 @@ Execution trace: Array.dfy(95,18): Error: assertion violation Execution trace: (0,0): anon0 -Array.dfy(107,6): Error: insufficient reads clause to read array element +Array.dfy(110,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon7_Else (0,0): anon8_Then (0,0): anon9_Then -Array.dfy(115,6): Error: insufficient reads clause to read array element +Array.dfy(118,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon7_Else (0,0): anon8_Then (0,0): anon9_Then -Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause +Array.dfy(134,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 -Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause +Array.dfy(141,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 60854f63..5f366d10 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -93,6 +93,9 @@ class A { assert y[8] == 30; assert y[90] + y[91] + y[0] + 20 == y.Length; assert y[93] == 24; // error (it's 25) + + y[..] := 4; // assign to all elements. + assert forall i :: 0 <= i < y.Length ==> y[i] == 4; } } -- cgit v1.2.3 From dae4b7981cc7af0c10dde91b0d095ad828f9c706 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Wed, 13 Jul 2011 13:20:05 -0700 Subject: Added multiset from sequence axioms, removed array range RHSs. Fixed issue with duplicate array.Length functions in generated Boogie file. --- Binaries/DafnyPrelude.bpl | 56 ++++++++++++++++++++------------- Dafny/Resolver.cs | 75 ++++++++++++++++++++++----------------------- Dafny/Translator.cs | 48 +++++++++++++++++++++-------- Test/dafny0/AdvancedLHS.dfy | 1 - Test/dafny0/Array.dfy | 35 +++++++-------------- 5 files changed, 117 insertions(+), 98 deletions(-) (limited to 'Test') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index e11acf26..37b972d0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -131,6 +131,8 @@ function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T; // union-ing is the sum of the contents axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] } MultiSet#Union(a,b)[o] == a[o] + b[o]); +axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Union(a,b) } + MultiSet#Union(a,b) == MultiSet#Union(b,a)); // two containment axioms axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } @@ -140,9 +142,8 @@ axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] } // symmetry axiom axiom (forall a, b: MultiSet T :: { MultiSet#Union(a, b) } - MultiSet#Disjoint(a, b) ==> - MultiSet#Difference(MultiSet#Union(a, b), a) == b && - MultiSet#Difference(MultiSet#Union(a, b), b) == a); + MultiSet#Difference(MultiSet#Union(a, b), a) == b && + MultiSet#Difference(MultiSet#Union(a, b), b) == a); function MultiSet#Intersection(MultiSet T, MultiSet T): MultiSet T; axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] } @@ -183,9 +184,17 @@ axiom (forall s: Set T, a: T :: { MultiSet#FromSet(s)[a] } (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) && (MultiSet#FromSet(s)[a] == 1 <==> s[a])); -// conversion to a multiset. each element in the original set has duplicity 1. +// conversion to a multiset, from a sequence. function MultiSet#FromSeq(Seq T): MultiSet T; -// no axioms yet. +axiom (forall s: Seq T, v: T :: + { MultiSet#FromSeq(Seq#Build(s, v)) } + MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v) + ); +axiom (MultiSet#FromSeq(Seq#Empty(): Seq BoxType) == MultiSet#Empty()); +axiom (forall a: Seq T, b: Seq T :: + { MultiSet#FromSeq(Seq#Append(a, b)) } + MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) && + MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(b), MultiSet#FromSeq(a))); // --------------------------------------------------------------- // -- Axiomatization of sequences -------------------------------- @@ -203,9 +212,12 @@ axiom (forall s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#E function Seq#Singleton(T): Seq T; axiom (forall t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1); -function Seq#Build(s: Seq T, index: int, val: T, newLength: int): Seq T; -axiom (forall s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) } - 0 <= len ==> Seq#Length(Seq#Build(s,i,v,len)) == len); +function Seq#Build(s: Seq T, val: T): Seq T; +axiom (forall s: Seq T, v: T :: { Seq#Length(Seq#Build(s,v)) } + Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s)); +axiom (forall s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) } + (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) && + (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i))); function Seq#Append(Seq T, Seq T): Seq T; axiom (forall s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) } @@ -216,10 +228,6 @@ axiom (forall t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Single axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) && (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); -axiom (forall s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) } - 0 <= n && n < len ==> - (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) && - (i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n))); function Seq#Update(Seq T, int, T): Seq T; axiom (forall s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } @@ -240,16 +248,11 @@ axiom (forall s0: Seq T, s1: Seq T, x: T :: { Seq#Contains(Seq#Append(s0, s1), x) } Seq#Contains(Seq#Append(s0, s1), x) <==> Seq#Contains(s0, x) || Seq#Contains(s1, x)); -axiom (forall i: int, v: T, len: int, x: T :: - { Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) } - 0 <= i && i < len ==> - (Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) <==> x == v)); -axiom (forall s: Seq T, i0: int, v0: T, len0: int, i1: int, v1: T, len1: int, x: T :: - { Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) } - 0 <= i0 && i0 < len0 && len0 <= i1 && i1 < len1 ==> - (Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) <==> - v1 == x || - Seq#Contains(Seq#Build(s, i0, v0, len0), x))); + +axiom (forall s: Seq T, v: T, x: T :: + { Seq#Contains(Seq#Build(s, v), x) } + Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x))); + axiom (forall s: Seq T, n: int, x: T :: { Seq#Contains(Seq#Take(s, n), x) } Seq#Contains(Seq#Take(s, n), x) <==> @@ -299,6 +302,11 @@ axiom (forall s, t: Seq T :: Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t); +function Seq#FromArray(h: HeapType, a: ref): Seq BoxType; +axiom (forall h: HeapType, a: ref :: { Seq#Length(Seq#FromArray(h,a)) } Seq#Length(Seq#FromArray(h, a)) == array.Length(a)); +axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType } + (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); + // --------------------------------------------------------------- // -- Boxing and unboxing ---------------------------------------- // --------------------------------------------------------------- @@ -328,6 +336,7 @@ const unique class.int: ClassName; const unique class.bool: ClassName; const unique class.set: ClassName; const unique class.seq: ClassName; +const unique class.multiset: ClassName; function /*{:never_pattern true}*/ dtype(ref): ClassName; function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName; @@ -435,6 +444,9 @@ axiom (forall r: ref, h: HeapType :: // -- Arrays ----------------------------------------------------- // --------------------------------------------------------------- +function array.Length(a: ref): int; +axiom (forall o: ref :: 0 <= array.Length(o)); + procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType); modifies $Heap; ensures $HeapSucc(old($Heap), $Heap); diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 2b3128ae..1321a987 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -1304,15 +1304,14 @@ namespace Microsoft.Dafny { // LHS is fine, provided the "sequence" is really an array if (lhsResolvedSuccessfully) { Contract.Assert(slhs.Seq.Type != null); - Type elementType = new InferredTypeProxy(); - if (!UnifyTypes(slhs.Seq.Type, builtIns.ArrayType(1, elementType))) { + if (!UnifyTypes(slhs.Seq.Type, builtIns.ArrayType(1, new InferredTypeProxy()))) { Error(slhs.Seq, "LHS of array assignment must denote an array element (found {0})", slhs.Seq.Type); } if (specContextOnly) { Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); } - if (!slhs.SelectOne && !(s.Rhs is ExprRhs)) { - Error(stmt, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable"); + if (!slhs.SelectOne) { + Error(stmt, "cannot assign to multiple array elements (try a foreach)."); } } @@ -1328,43 +1327,43 @@ namespace Microsoft.Dafny { s.IsGhost = lvalueIsGhost; Type lhsType = s.Lhs.Type; if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) { - Contract.Assert(lhsType.IsArrayType); - lhsType = UserDefinedType.ArrayElementType(lhsType); - } - if (s.Rhs is ExprRhs) { - ExprRhs rr = (ExprRhs)s.Rhs; - ResolveExpression(rr.Expr, true); - if (!lvalueIsGhost) { - CheckIsNonGhost(rr.Expr); - } - Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression - if (!UnifyTypes(lhsType, rr.Expr.Type)) { - Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType); - } - } else if (s.Rhs is TypeRhs) { - TypeRhs rr = (TypeRhs)s.Rhs; - Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method); - if (!lvalueIsGhost) { - if (rr.ArrayDimensions != null) { - foreach (var dim in rr.ArrayDimensions) { - CheckIsNonGhost(dim); - } + Error(stmt, "cannot assign to multiple array elements (try a foreach)."); + //lhsType = UserDefinedType.ArrayElementType(lhsType); + } else { + if (s.Rhs is ExprRhs) { + ExprRhs rr = (ExprRhs)s.Rhs; + ResolveExpression(rr.Expr, true); + if (!lvalueIsGhost) { + CheckIsNonGhost(rr.Expr); } - if (rr.InitCall != null) { - foreach (var arg in rr.InitCall.Args) { - CheckIsNonGhost(arg); + Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression + if (!UnifyTypes(lhsType, rr.Expr.Type)) { + Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType); + } + } else if (s.Rhs is TypeRhs) { + TypeRhs rr = (TypeRhs)s.Rhs; + Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method); + if (!lvalueIsGhost) { + if (rr.ArrayDimensions != null) { + foreach (var dim in rr.ArrayDimensions) { + CheckIsNonGhost(dim); + } + } + if (rr.InitCall != null) { + foreach (var arg in rr.InitCall.Args) { + CheckIsNonGhost(arg); + } } } + if (!UnifyTypes(lhsType, t)) { + Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType); + } + } else if (s.Rhs is HavocRhs) { + // nothing else to do + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS } - if (!UnifyTypes(lhsType, t)) { - Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType); - } - } else if (s.Rhs is HavocRhs) { - // nothing else to do - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS } - } else if (stmt is VarDecl) { VarDecl s = (VarDecl)stmt; if (s.OptionalType != null) { @@ -2340,7 +2339,7 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - ResolveSeqSelectExpr(e, twoState, false); + ResolveSeqSelectExpr(e, twoState, true); } else if (expr is MultiSelectExpr) { MultiSelectExpr e = (MultiSelectExpr)expr; @@ -3554,7 +3553,7 @@ namespace Microsoft.Dafny { if (e.SelectOne) { e.Type = elementType; } else { - e.Type = e.Seq.Type; + e.Type = new SeqType(elementType); } } } diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index dacbf143..60a40f57 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -44,6 +44,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type TickType; private readonly Bpl.TypeSynonymDecl setTypeCtor; private readonly Bpl.TypeSynonymDecl multiSetTypeCtor; + public readonly Bpl.Function ArrayLength; private readonly Bpl.TypeCtorDecl seqTypeCtor; readonly Bpl.TypeCtorDecl fieldName; public readonly Bpl.Type HeapType; @@ -60,6 +61,7 @@ namespace Microsoft.Dafny { Contract.Invariant(TickType != null); Contract.Invariant(setTypeCtor != null); Contract.Invariant(multiSetTypeCtor != null); + Contract.Invariant(ArrayLength != null); Contract.Invariant(seqTypeCtor != null); Contract.Invariant(fieldName != null); Contract.Invariant(HeapType != null); @@ -111,7 +113,7 @@ namespace Microsoft.Dafny { } public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType, - Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType, + Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType, Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId, Bpl.Constant allocField) { @@ -136,6 +138,7 @@ namespace Microsoft.Dafny { this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq()); this.setTypeCtor = setTypeCtor; this.multiSetTypeCtor = multiSetTypeCtor; + this.ArrayLength = arrayLength; this.seqTypeCtor = seqTypeCtor; this.fieldName = fieldNameType; this.HeapType = heap.TypedIdent.Type; @@ -158,6 +161,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl refType = null; Bpl.TypeSynonymDecl setTypeCtor = null; Bpl.TypeSynonymDecl multiSetTypeCtor = null; + Bpl.Function arrayLength = null; Bpl.TypeCtorDecl seqTypeCtor = null; Bpl.TypeCtorDecl fieldNameType = null; Bpl.TypeCtorDecl classNameType = null; @@ -167,7 +171,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl tickType = null; Bpl.GlobalVariable heap = null; Bpl.Constant allocField = null; - foreach (Bpl.Declaration d in prog.TopLevelDeclarations) { + foreach (var d in prog.TopLevelDeclarations) { if (d is Bpl.TypeCtorDecl) { Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d; if (dt.Name == "Seq") { @@ -205,6 +209,10 @@ namespace Microsoft.Dafny { if (v.Name == "$Heap") { heap = v; } + } else if (d is Bpl.Function) { + var f = (Bpl.Function)d; + if (f.Name == "array.Length") + arrayLength = f; } } if (seqTypeCtor == null) { @@ -213,6 +221,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Set"); } else if (multiSetTypeCtor == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet"); + } else if (arrayLength == null) { + Console.WriteLine("Error: Dafny prelude is missing declaration of function array.Length"); } else if (fieldNameType == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of type Field"); } else if (classNameType == null) { @@ -233,7 +243,7 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); } else { return new PredefinedDecls(refType, boxType, tickType, - setTypeCtor, multiSetTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId, + setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId, allocField); } return null; @@ -506,7 +516,8 @@ namespace Microsoft.Dafny { sink.TopLevelDeclarations.Add(fc); } else { Bpl.Function ff = GetReadonlyField(f); - sink.TopLevelDeclarations.Add(ff); + if (ff != predef.ArrayLength) + sink.TopLevelDeclarations.Add(ff); } AddAllocationAxiom(f); @@ -1656,7 +1667,7 @@ namespace Microsoft.Dafny { } } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; - bool isSequence = e.Seq.Type is SeqType; + //bool isSequence = e.Seq.Type is SeqType; Bpl.Expr total = CanCallAssumption(e.Seq, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); Bpl.Expr e0 = null; @@ -2396,7 +2407,7 @@ namespace Microsoft.Dafny { if (a == null) { return null; } - Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too. + Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : (ct is SeqType ? "class.seq" : "class.multiset"), predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too. return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a); } else { UserDefinedType ct = (UserDefinedType)type; @@ -2448,6 +2459,10 @@ namespace Microsoft.Dafny { if (fieldFunctions.TryGetValue(f, out ff)) { Contract.Assert(ff != null); } else { + if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude. + fieldFunctions.Add(f, predef.ArrayLength); + return predef.ArrayLength; + } // function f(Ref): ty; Bpl.Type ty = TrType(f.Type); Bpl.VariableSeq args = new Bpl.VariableSeq(); @@ -4680,7 +4695,7 @@ namespace Microsoft.Dafny { } return s; - } else if (expr is MultiSetDisplayExpr) { //^^^ todo: add multiset to BuiltinFunction + } else if (expr is MultiSetDisplayExpr) { MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr; Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType); foreach (Expression ee in e.Elements) { @@ -4694,8 +4709,8 @@ namespace Microsoft.Dafny { Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType); int i = 0; foreach (Expression ee in e.Elements) { - Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type)); - s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, Bpl.Expr.Literal(i), ss, Bpl.Expr.Literal(i+1)); + Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type)); + s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt); i++; } return s; @@ -4711,14 +4726,13 @@ namespace Microsoft.Dafny { result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new Bpl.ExprSeq(obj)); } return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type)); - + } else if (expr is SeqSelectExpr) { SeqSelectExpr e = (SeqSelectExpr)expr; Bpl.Expr seq = TrExpr(e.Seq); Type elmtType; Contract.Assert(e.Seq.Type != null); // the expression has been successfully resolved if (e.Seq.Type.IsArrayType) { - Contract.Assert(e.SelectOne); // resolution enforces that a non-unit array selections is allowed only as an assignment LHS elmtType = UserDefinedType.ArrayElementType(e.Seq.Type); } else { elmtType = ((SeqType)e.Seq.Type).Arg; @@ -4740,13 +4754,16 @@ namespace Microsoft.Dafny { } return x; } else { + if (e.Seq.Type.IsArrayType) { + seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqFromArray, elType, HeapExpr, seq); + } if (e1 != null) { seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqTake, elType, seq, e1); } if (e0 != null) { seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0); } - // if e0 == null && e1 == null, then we have the identity operation seq[..]; + // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq; return seq; } @@ -5489,6 +5506,7 @@ namespace Microsoft.Dafny { SeqTake, SeqEqual, SeqSameUntil, + SeqFromArray, IndexField, MultiIndexField, @@ -5627,7 +5645,7 @@ namespace Microsoft.Dafny { return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType); } case BuiltinFunction.SeqBuild: - Contract.Assert(args.Length == 4); + Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation != null); return FunctionCall(tok, "Seq#Build", predef.SeqType(tok, typeInstantiation), args); case BuiltinFunction.SeqAppend: @@ -5662,6 +5680,10 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 3); Contract.Assert(typeInstantiation == null); return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args); + case BuiltinFunction.SeqFromArray: + Contract.Assert(args.Length == 2); + Contract.Assert(typeInstantiation != null); + return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args); case BuiltinFunction.IndexField: Contract.Assert(args.Length == 1); diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy index cc07cbb5..f1fc7d48 100644 --- a/Test/dafny0/AdvancedLHS.dfy +++ b/Test/dafny0/AdvancedLHS.dfy @@ -34,7 +34,6 @@ class C { if (a != null && 10 <= a.Length) { a[2] := new C; - a[4..8] := null; a[3] := *; } if (b != null && 10 <= b.Length0 && 20 <= b.Length1) { diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 5f366d10..1a18be6d 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -72,30 +72,17 @@ class A { } method Q() { - var y := new object[100]; - y[5] := null; - y[0..] := null; - y[..83] := null; - y[0..y.Length] := null; - } - - method R() { - var y := new int[100]; - y[55] := 80; - y[10..] := 25; - y[..83] := 30; - y[50..60] := 35; - y[55] := 90; - - assert y[54] == 35; - assert y[55] == 90; - assert y[83] == 25; - assert y[8] == 30; - assert y[90] + y[91] + y[0] + 20 == y.Length; - assert y[93] == 24; // error (it's 25) - - y[..] := 4; // assign to all elements. - assert forall i :: 0 <= i < y.Length ==> y[i] == 4; + var a := new int[5]; + y[0],y[1],y[2],y[3],y[4] := 0,1,2,3,4; + + assert [1,2,3,4] == y[1..]; + assert [1,2,3,4] == y[1.. y.Length]; + assert [1] == y[1..2]; + assert [0,1] == y[..2]; + assert [0,1] == y[0..2]; + assert forall i :: 0 <= i <= y.Length ==> [] == y[i..i]; + assert [0,1,2,3,4] == y[..]; + assert forall i :: 0 <= i < y.Length ==> y[i] == i; } } -- cgit v1.2.3 From bd0939ffe92812966dfe2aac15d28cc1e3c37b42 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Thu, 14 Jul 2011 19:04:48 -0700 Subject: Fixed failing regression tests. --- Test/dafny0/Answer | 221 +++++++++++++++++++++------------------- Test/dafny0/Array.dfy | 18 ++-- Test/dafny0/Definedness.dfy | 16 ++- Test/dafny0/NatTypes.dfy | 3 + Test/dafny0/Termination.dfy | 5 + Test/dafny0/TypeAntecedents.dfy | 4 +- Test/dafny0/TypeParameters.dfy | 23 ++++- 7 files changed, 169 insertions(+), 121 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a6f1e9b7..d9294f1a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -74,12 +74,14 @@ TypeTests.dfy(58,8): Error: Duplicate local-variable name: x TypeTests.dfy(61,6): Error: Duplicate local-variable name: y TypeTests.dfy(68,17): Error: member F in type C does not refer to a method TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments -TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable -TypeTests.dfy(79,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable +TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach). +TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach). +TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach). +TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach). TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type -21 resolution/type errors detected in TypeTests.dfy +23 resolution/type errors detected in TypeTests.dfy -------------------- NatTypes.dfy -------------------- NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative @@ -102,20 +104,20 @@ NatTypes.dfy(40,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon4_Then -NatTypes.dfy(54,16): Error: assertion violation +NatTypes.dfy(57,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then -NatTypes.dfy(68,16): Error: assertion violation +NatTypes.dfy(71,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon5_Else (0,0): anon6_Then -NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative +NatTypes.dfy(89,19): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 (0,0): anon3_Then -NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative +NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon6_Else (0,0): anon7_Else @@ -231,149 +233,167 @@ Execution trace: Definedness.dfy(50,18): Error: target object may be null Execution trace: (0,0): anon0 -Definedness.dfy(55,18): Error: target object may be null +Definedness.dfy(51,3): Error BP5003: A postcondition might not hold on this return path. +Definedness.dfy(50,22): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -Definedness.dfy(77,7): Error: target object may be null +Definedness.dfy(57,18): Error: target object may be null Execution trace: (0,0): anon0 -Definedness.dfy(78,5): Error: possible violation of function precondition +Definedness.dfy(58,3): Error BP5003: A postcondition might not hold on this return path. +Definedness.dfy(57,22): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -Definedness.dfy(79,10): Error: possible violation of function precondition +Definedness.dfy(65,3): Error BP5003: A postcondition might not hold on this return path. +Definedness.dfy(64,22): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 -Definedness.dfy(84,14): Error: possible division by zero +Definedness.dfy(85,7): Error: target object may be null Execution trace: (0,0): anon0 -Definedness.dfy(84,23): Error: possible division by zero +Definedness.dfy(86,5): Error: possible violation of function precondition Execution trace: (0,0): anon0 -Definedness.dfy(85,15): Error: possible division by zero +Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause Execution trace: (0,0): anon0 -Definedness.dfy(90,12): Error: possible division by zero +Definedness.dfy(86,10): Error: target object may be null Execution trace: (0,0): anon0 -Definedness.dfy(97,15): Error: possible division by zero +Definedness.dfy(87,10): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(97,5): anon8_LoopHead +Definedness.dfy(92,14): Error: possible division by zero +Execution trace: + (0,0): anon0 +Definedness.dfy(92,23): Error: possible division by zero +Execution trace: + (0,0): anon0 +Definedness.dfy(93,15): Error: possible division by zero +Execution trace: + (0,0): anon0 +Definedness.dfy(98,12): Error: possible division by zero +Execution trace: + (0,0): anon0 +Definedness.dfy(105,15): Error: possible division by zero +Execution trace: + (0,0): anon0 + Definedness.dfy(105,5): anon8_LoopHead (0,0): anon8_LoopBody - Definedness.dfy(97,5): anon9_Else + Definedness.dfy(105,5): anon9_Else (0,0): anon3 -Definedness.dfy(106,23): Error: possible violation of function precondition +Definedness.dfy(114,23): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(105,5): anon13_LoopHead + Definedness.dfy(113,5): anon13_LoopHead (0,0): anon13_LoopBody (0,0): anon14_Then -Definedness.dfy(112,17): Error: possible violation of function precondition +Definedness.dfy(120,17): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(105,5): anon13_LoopHead + Definedness.dfy(113,5): anon13_LoopHead (0,0): anon13_LoopBody - Definedness.dfy(105,5): anon14_Else + Definedness.dfy(113,5): anon14_Else (0,0): anon3 (0,0): anon15_Then (0,0): anon6 - Definedness.dfy(111,5): anon16_LoopHead + Definedness.dfy(119,5): anon16_LoopHead (0,0): anon16_LoopBody (0,0): anon17_Then -Definedness.dfy(122,17): Error: possible violation of function precondition +Definedness.dfy(130,17): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(121,5): anon7_LoopHead + Definedness.dfy(129,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry. +Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry. Execution trace: (0,0): anon0 -Definedness.dfy(123,17): Error: possible violation of function precondition +Definedness.dfy(131,17): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(121,5): anon7_LoopHead + Definedness.dfy(129,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -Definedness.dfy(132,15): Error: possible division by zero +Definedness.dfy(140,15): Error: possible division by zero Execution trace: (0,0): anon0 - Definedness.dfy(132,5): anon9_LoopHead + Definedness.dfy(140,5): anon9_LoopHead (0,0): anon9_LoopBody - Definedness.dfy(132,5): anon10_Else + Definedness.dfy(140,5): anon10_Else (0,0): anon3 -Definedness.dfy(151,15): Error: possible division by zero +Definedness.dfy(159,15): Error: possible division by zero Execution trace: (0,0): anon0 - Definedness.dfy(145,5): anon17_LoopHead + Definedness.dfy(153,5): anon17_LoopHead (0,0): anon17_LoopBody - Definedness.dfy(145,5): anon18_Else + Definedness.dfy(153,5): anon18_Else (0,0): anon3 (0,0): anon19_Then (0,0): anon5 (0,0): anon20_Then (0,0): anon8 - Definedness.dfy(151,5): anon21_LoopHead + Definedness.dfy(159,5): anon21_LoopHead (0,0): anon21_LoopBody - Definedness.dfy(151,5): anon22_Else + Definedness.dfy(159,5): anon22_Else (0,0): anon11 -Definedness.dfy(170,17): Error: possible violation of function precondition +Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry. +Execution trace: + (0,0): anon0 +Definedness.dfy(178,17): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Definedness.dfy(162,5): anon19_LoopHead + Definedness.dfy(170,5): anon19_LoopHead (0,0): anon19_LoopBody - Definedness.dfy(162,5): anon20_Else + Definedness.dfy(170,5): anon20_Else (0,0): anon3 (0,0): anon21_Then (0,0): anon6 - Definedness.dfy(169,5): anon22_LoopHead + Definedness.dfy(177,5): anon22_LoopHead (0,0): anon22_LoopBody (0,0): anon23_Then (0,0): anon24_Then (0,0): anon11 -Definedness.dfy(191,24): Error: possible violation of function precondition +Definedness.dfy(199,24): Error: possible violation of function precondition Execution trace: (0,0): anon0 -Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause +Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause Execution trace: (0,0): anon0 -Definedness.dfy(195,33): Error: range expression must be well defined +Definedness.dfy(203,33): Error: range expression must be well defined Execution trace: (0,0): anon0 -Definedness.dfy(201,18): Error: RHS of assignment must be well defined +Definedness.dfy(218,19): Error: possible division by zero Execution trace: (0,0): anon0 -Definedness.dfy(210,19): Error: possible division by zero -Execution trace: - (0,0): anon0 - Definedness.dfy(208,5): anon7_LoopHead + Definedness.dfy(216,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry. +Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry. Execution trace: (0,0): anon0 -Definedness.dfy(210,28): Error: possible division by zero +Definedness.dfy(218,28): Error: possible division by zero Execution trace: (0,0): anon0 - Definedness.dfy(208,5): anon7_LoopHead + Definedness.dfy(216,5): anon7_LoopHead (0,0): anon7_LoopBody (0,0): anon8_Then -Definedness.dfy(231,46): Error: possible violation of function postcondition +Definedness.dfy(239,46): Error: possible violation of function postcondition Execution trace: (0,0): anon0 (0,0): anon5_Else -Definedness.dfy(238,22): Error: target object may be null +Definedness.dfy(246,22): Error: target object may be null Execution trace: (0,0): anon5_Then (0,0): anon2 (0,0): anon6_Then -Definedness.dfy(254,24): Error: possible violation of function postcondition +Definedness.dfy(262,24): Error: possible violation of function postcondition Execution trace: (0,0): anon7_Then (0,0): anon2 (0,0): anon8_Else -Dafny program verifier finished with 23 verified, 34 errors +Dafny program verifier finished with 23 verified, 39 errors -------------------- FunctionSpecifications.dfy -------------------- FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition @@ -484,27 +504,24 @@ Execution trace: (0,0): anon5_Then (0,0): anon2 (0,0): anon6_Then -Array.dfy(95,18): Error: assertion violation -Execution trace: - (0,0): anon0 -Array.dfy(110,6): Error: insufficient reads clause to read array element +Array.dfy(97,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon7_Else (0,0): anon8_Then (0,0): anon9_Then -Array.dfy(118,6): Error: insufficient reads clause to read array element +Array.dfy(105,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon7_Else (0,0): anon8_Then (0,0): anon9_Then -Array.dfy(134,6): Error: assignment may update an array element not in the enclosing context's modifies clause +Array.dfy(121,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 -Array.dfy(141,6): Error: assignment may update an array element not in the enclosing context's modifies clause +Array.dfy(128,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 -Dafny program verifier finished with 22 verified, 11 errors +Dafny program verifier finished with 21 verified, 10 errors -------------------- MultiDimArray.dfy -------------------- MultiDimArray.dfy(53,21): Error: assertion violation @@ -812,61 +829,61 @@ Execution trace: Dafny program verifier finished with 18 verified, 10 errors -------------------- Termination.dfy -------------------- -Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop +Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop Execution trace: (0,0): anon0 - Termination.dfy(100,3): anon7_LoopHead + Termination.dfy(105,3): anon7_LoopHead (0,0): anon7_LoopBody - Termination.dfy(100,3): anon8_Else + Termination.dfy(105,3): anon8_Else (0,0): anon3 - Termination.dfy(100,3): anon9_Else + Termination.dfy(105,3): anon9_Else (0,0): anon5 -Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop +Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop Execution trace: (0,0): anon0 - Termination.dfy(108,3): anon9_LoopHead + Termination.dfy(113,3): anon9_LoopHead (0,0): anon9_LoopBody - Termination.dfy(108,3): anon10_Else + Termination.dfy(113,3): anon10_Else (0,0): anon11_Then (0,0): anon5 - Termination.dfy(108,3): anon12_Else + Termination.dfy(113,3): anon12_Else (0,0): anon7 -Termination.dfy(117,3): Error: decreases expression might not decrease +Termination.dfy(122,3): Error: decreases expression might not decrease Execution trace: (0,0): anon0 - Termination.dfy(117,3): anon9_LoopHead + Termination.dfy(122,3): anon9_LoopHead (0,0): anon9_LoopBody - Termination.dfy(117,3): anon10_Else + Termination.dfy(122,3): anon10_Else (0,0): anon11_Then (0,0): anon5 - Termination.dfy(117,3): anon12_Else + Termination.dfy(122,3): anon12_Else (0,0): anon7 -Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration +Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration Execution trace: (0,0): anon0 - Termination.dfy(117,3): anon9_LoopHead + Termination.dfy(122,3): anon9_LoopHead (0,0): anon9_LoopBody - Termination.dfy(117,3): anon10_Else + Termination.dfy(122,3): anon10_Else (0,0): anon11_Then (0,0): anon5 - Termination.dfy(117,3): anon12_Else + Termination.dfy(122,3): anon12_Else (0,0): anon7 -Termination.dfy(246,35): Error: cannot prove termination; try supplying a decreases clause +Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon6_Else (0,0): anon7_Else (0,0): anon8_Then -Termination.dfy(286,3): Error: decreases expression might not decrease +Termination.dfy(291,3): Error: decreases expression might not decrease Execution trace: (0,0): anon0 - Termination.dfy(286,3): anon10_LoopHead + Termination.dfy(291,3): anon10_LoopHead (0,0): anon10_LoopBody - Termination.dfy(286,3): anon11_Else - Termination.dfy(286,3): anon12_Else + Termination.dfy(291,3): anon11_Else + Termination.dfy(291,3): anon12_Else (0,0): anon13_Else (0,0): anon8 -Dafny program verifier finished with 44 verified, 6 errors +Dafny program verifier finished with 45 verified, 6 errors -------------------- DTypes.dfy -------------------- DTypes.dfy(15,14): Error: assertion violation @@ -898,46 +915,46 @@ Execution trace: Dafny program verifier finished with 27 verified, 6 errors -------------------- TypeParameters.dfy -------------------- -TypeParameters.dfy(41,22): Error: assertion violation +TypeParameters.dfy(44,22): Error: assertion violation Execution trace: (0,0): anon0 -TypeParameters.dfy(63,27): Error: assertion violation +TypeParameters.dfy(66,27): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Then (0,0): anon2 -TypeParameters.dfy(130,12): Error: assertion violation -TypeParameters.dfy(130,28): Related location: Related location +TypeParameters.dfy(138,12): Error: assertion violation +TypeParameters.dfy(138,28): Related location: Related location Execution trace: (0,0): anon0 (0,0): anon14_Then - TypeParameters.dfy(130,32): anon15_Else + TypeParameters.dfy(138,32): anon15_Else (0,0): anon5 -TypeParameters.dfy(132,12): Error: assertion violation -TypeParameters.dfy(132,33): Related location: Related location +TypeParameters.dfy(140,12): Error: assertion violation +TypeParameters.dfy(140,33): Related location: Related location Execution trace: (0,0): anon0 (0,0): anon17_Then - TypeParameters.dfy(132,37): anon18_Else + TypeParameters.dfy(140,37): anon18_Else (0,0): anon11 -TypeParameters.dfy(146,15): Error BP5005: This loop invariant might not be maintained by the loop. -TypeParameters.dfy(146,38): Related location: Related location +TypeParameters.dfy(154,15): Error BP5005: This loop invariant might not be maintained by the loop. +TypeParameters.dfy(154,38): Related location: Related location Execution trace: (0,0): anon0 - TypeParameters.dfy(139,3): anon17_LoopHead + TypeParameters.dfy(147,3): anon17_LoopHead (0,0): anon17_LoopBody - TypeParameters.dfy(139,3): anon18_Else + TypeParameters.dfy(147,3): anon18_Else (0,0): anon5 (0,0): anon20_Then (0,0): anon8 - TypeParameters.dfy(145,3): anon21_LoopHead + TypeParameters.dfy(153,3): anon21_LoopHead (0,0): anon21_LoopBody - TypeParameters.dfy(145,3): anon22_Else + TypeParameters.dfy(153,3): anon22_Else (0,0): anon13 - TypeParameters.dfy(145,3): anon24_Else + TypeParameters.dfy(153,3): anon24_Else (0,0): anon15 -Dafny program verifier finished with 33 verified, 5 errors +Dafny program verifier finished with 35 verified, 5 errors -------------------- Datatypes.dfy -------------------- Datatypes.dfy(79,20): Error: assertion violation diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 1a18be6d..f667e699 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -73,16 +73,16 @@ class A { method Q() { var a := new int[5]; - y[0],y[1],y[2],y[3],y[4] := 0,1,2,3,4; + a[0],a[1],a[2],a[3],a[4] := 0,1,2,3,4; - assert [1,2,3,4] == y[1..]; - assert [1,2,3,4] == y[1.. y.Length]; - assert [1] == y[1..2]; - assert [0,1] == y[..2]; - assert [0,1] == y[0..2]; - assert forall i :: 0 <= i <= y.Length ==> [] == y[i..i]; - assert [0,1,2,3,4] == y[..]; - assert forall i :: 0 <= i < y.Length ==> y[i] == i; + assert [1,2,3,4] == a[1..]; + assert [1,2,3,4] == a[1.. a.Length]; + assert [1] == a[1..2]; + assert [0,1] == a[..2]; + assert [0,1] == a[0..2]; + assert forall i :: 0 <= i <= a.Length ==> [] == a[i..i]; + assert [0,1,2,3,4] == a[..]; + assert forall i :: 0 <= i < a.Length ==> a[i] == i; } } diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 2063eec4..44b54f3d 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -48,27 +48,35 @@ class SoWellformed { requires next != null; modifies this; ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null) + { + } method Q(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed) requires next != null; modifies s; ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null) - + { + + } method R(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed) requires next != null && this !in s; modifies s; ensures next.xyz < 100; // fine + { + + } } // ---------------------- welldefinedness checks for statements ------------------- class StatementTwoShoes { var x: int; - + var s: StatementTwoShoes; function method F(b: int): StatementTwoShoes requires 0 <= b; + reads this; { - this + s } method M(p: StatementTwoShoes, a: int) @@ -175,7 +183,7 @@ class StatementTwoShoes { } function G(w: int): int { 5 } - function method H(x: int): int + function method H(x: int): int { -x } method V(s: set, a: int, b: int) modifies s; diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index e56b4122..47bc22e1 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -43,6 +43,9 @@ method Generic(i: int, t0: T, t1: T) returns (r: T) { } function method FenEric(t0: T, t1: T): T +{ + t1 +} datatype Pair = Pr(T, T); diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index f31935af..1482dc24 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -90,6 +90,11 @@ class Termination { method Traverse(a: List) returns (val: T, b: List) requires a != List.Nil; ensures a == List.Cons(val, b); + { + match a { + case Cons(v, r) => val := v; b := r; + } + } } datatype List = Nil | Cons(T, List); diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 710e9838..5982a9e6 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -87,8 +87,8 @@ method N() returns (k: MyClass) { k := new MyClass; } - -function NF(): MyClass +var a: MyClass; +function NF(): MyClass reads this; { a } function TakesADatatype(a: List): int { 12 } diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 8f3f8b87..d6804661 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -14,10 +14,13 @@ class C { { var t := F(3,u) && F(this,u); var kz := M(t,u); - assert kz && (G() || !G()); + var a := G(); + assert kz && (a || !a); + } + method G() returns (a: Y) + { + } - - function G(): Y } class SetTest { @@ -101,6 +104,9 @@ class CClient { static function IsCelebrity(c: Person, people: set): bool requires c == c || c in people; +{ + false +} method FindCelebrity3(people: set, ghost c: int) requires IsCelebrity(c, people); // once upon a time, this caused the translator to produce bad Boogie @@ -112,7 +118,9 @@ method FindCelebrity3(people: set, ghost c: int) static function F(c: int, people: set): bool requires IsCelebrity(c, people); - +{ + false +} function RogerThat(g: G): G { g @@ -154,7 +162,14 @@ method LoopyRoger(n: int) class TyKn_C { var x: T; function G(): T + reads this; + { + x + } method M() returns (t: T) + { + + } } class TyKn_K { -- cgit v1.2.3 From 47c23bd0d7e71722a94b8df660c0314381b4263a Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Fri, 15 Jul 2011 17:42:55 -0700 Subject: Fixed regression test failures due to removal of bodiless methods and functions. --- Test/VSI-Benchmarks/Answer | 12 ----- Test/VSI-Benchmarks/runtest.bat | 4 +- Test/dafny0/Answer | 4 ++ Test/dafny0/MultiSets.dfy | 103 ++++++++++++++++++++++++++++++++++++++++ Test/dafny0/runtest.bat | 2 +- Test/dafny1/Answer | 6 +-- Test/dafny1/Celebrity.dfy | 26 +++++++--- Test/dafny1/Rippling.dfy | 18 +++---- Test/dafny1/UltraFilter.dfy | 3 ++ 9 files changed, 146 insertions(+), 32 deletions(-) create mode 100644 Test/dafny0/MultiSets.dfy (limited to 'Test') diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 2a4587f4..e2456408 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -7,10 +7,6 @@ Dafny program verifier finished with 10 verified, 0 errors Dafny program verifier finished with 6 verified, 0 errors --------------------- b3.dfy -------------------- - -Dafny program verifier finished with 10 verified, 0 errors - -------------------- b4.dfy -------------------- Dafny program verifier finished with 11 verified, 0 errors @@ -22,11 +18,3 @@ Dafny program verifier finished with 22 verified, 0 errors -------------------- b6.dfy -------------------- Dafny program verifier finished with 21 verified, 0 errors - --------------------- b7.dfy -------------------- - -Dafny program verifier finished with 23 verified, 0 errors - --------------------- b8.dfy -------------------- - -Dafny program verifier finished with 42 verified, 0 errors diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index a733a1c0..799e1d40 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -6,7 +6,9 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe set BPLEXE=%BOOGIEDIR%\Boogie.exe set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe -for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do ( +REM b3, b7 and b8 need reworking to not use body-less functions and methods. + +for %%f in (b1.dfy b2.dfy b4.dfy b5.dfy b6.dfy) do ( echo. echo -------------------- %%f -------------------- diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index d9294f1a..0723bcba 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1125,3 +1125,7 @@ Dafny program verifier finished with 6 verified, 0 errors CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable 2 resolution/type errors detected in CallStmtTests.dfy + +-------------------- MultiSets.dfy -------------------- + +Dafny program verifier finished with 22 verified, 0 errors diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy new file mode 100644 index 00000000..0bc1004f --- /dev/null +++ b/Test/dafny0/MultiSets.dfy @@ -0,0 +1,103 @@ + +method test1() +{ + var ms: multiset := multiset{1,1,1}; + var ms2: multiset := multiset{3}; + assert 1 in ms; + assert forall i :: i != 1 ==> i !in ms; // 1 is the only thing in ms. + + assert ((ms - multiset{1}) - multiset {1}) != multiset{}; // it has more than 2 ones + assert ((ms - multiset{1}) - multiset {1}) - multiset{1} == multiset{}; // and exactly three + + assert ms2 - ms == ms2; // set difference works correctly. + assert ms - multiset{1} == multiset{1,1}; + assert !(multiset{1} !! multiset{1}); + assert exists m :: !(m !! multiset{1}); + assert forall m :: m !! multiset{}; + + assert forall s :: (s == set x: int | x in ms :: x) ==> s == {1}; +} + +method test2(ms: multiset) +{ + var s := set x | x in ms :: x; // seems to be a reasonable conversion + assert forall x :: x in s <==> x in ms; + assert ms !! multiset{}; +} + +method test3(s: set) +{ + assert forall x :: x in s <==> x in multiset(s); +} +method test4(sq: seq, a: array) + requires a != null; + modifies a; +{ + assert sq == sq[..|sq|]; + assert sq == sq[0..]; + assert sq == sq[..]; + + assert a.Length >= 0; + var s := a[..]; +} + +method test5() +{ + assert multiset({1,1}) == multiset{1}; + assert multiset([1,1]) == multiset{1,1}; +} + +method test6(a: array, n: int, e: int) + requires a != null && 0 <= n < a.Length; + modifies a; + ensures multiset(a[..n+1]) == multiset(a[..n]) + multiset{e}; +{ + a[n] := e; + assert a[..n+1] == a[..n] + [e]; +} +method test7(a: array, i: int, j: int) + requires a != null && 0 <= i < j < a.Length; + modifies a; + ensures old(multiset(a[..])) == multiset(a[..]); + ensures a[j] == old (a[i]) && a[i] == old(a[j]); + ensures forall k :: 0 <= k < a.Length && k !in {i, j} ==> a[k] == old(a[k]); +{ + ghost var s := a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..]; + assert a[..] == s; + a[i], a[j] := a[j], a[i]; + assert a[..] == a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..]; + assert s == a[..i] + [old(a[i])] + a[i+1 .. j] + [old(a[j])] + a[j+1..]; +} +method test8(a: array, i: int, j: int) + requires a != null && 0 <= i < j < a.Length; + modifies a; + ensures old(multiset(a[..])) == multiset(a[..]); + ensures a[j] == old (a[i]) && a[i] == old(a[j]); + ensures forall k :: 0 <= k < a.Length && k !in {i, j} ==> a[k] == old(a[k]); +{ + a[i], a[j] := a[j], a[i]; +} +method test9(a: array, i: int, j: int, limit: int) + requires a != null && 0 <= i < j < limit <= a.Length; + modifies a; + ensures old(multiset(a[0..limit])) == multiset(a[0..limit]); + ensures a[j] == old (a[i]) && a[i] == old(a[j]); + ensures forall k :: 0 <= k < limit && k !in {i, j} ==> a[k] == old(a[k]); +{ + a[i], a[j] := a[j], a[i]; +} +method test10(s: seq) + requires |s| > 4; +{ + assert multiset( s[3 := 2] ) == multiset(s) - multiset{s[3]} + multiset{2}; + assert multiset( (s[2 := 1])[3 := 2] ) == (((multiset(s) - multiset{s[2]}) + multiset{1}) - multiset{s[3]}) + multiset{2}; + assert multiset( (s[2 := s[3]])[3 := s[2]] ) == (((multiset(s) - multiset{s[2]}) + multiset{s[3]}) - multiset{s[3]}) + multiset{s[2]}; +} + +method test11(a: array, n: int, c: int) + requires a != null && 0 <= c < n <= a.Length; + modifies a; + ensures multiset(a[c..n-1]) == multiset(a[c..n]) - multiset{a[n-1]}; +{ + +} \ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 7aa1b38e..8aaa143b 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy LoopModifies.dfy ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy - CallStmtTests.dfy) do ( + CallStmtTests.dfy MultiSets.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 %* %%f diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 5ee9f921..5bb746d8 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -85,12 +85,12 @@ Dafny program verifier finished with 29 verified, 0 errors -------------------- Rippling.dfy -------------------- -Dafny program verifier finished with 132 verified, 0 errors +Dafny program verifier finished with 122 verified, 0 errors -------------------- Celebrity.dfy -------------------- -Dafny program verifier finished with 10 verified, 0 errors +Dafny program verifier finished with 8 verified, 0 errors -------------------- UltraFilter.dfy -------------------- -Dafny program verifier finished with 19 verified, 0 errors +Dafny program verifier finished with 20 verified, 0 errors diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 21b895aa..a10c4324 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -1,15 +1,26 @@ // Celebrity example, inspired by the Rodin tutorial -static function method Knows(a: Person, b: Person): bool - requires a != b; // forbid asking about the reflexive case +class Person +{ + +} + +var pa: seq; -static function IsCelebrity(c: Person, people: set): bool +function method Knows(a: Person, b: Person): bool + reads this; + requires a != b; // forbid asking about the reflexive case +{ + exists i | 0 <= i && i < |pa| :: 0 <= i < |pa| / 2 ==> pa[2*i] == a && pa[2*i+1] == b +} +function IsCelebrity(c: Person, people: set): bool + reads this; { c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)) } -method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) requires (exists c :: IsCelebrity(c, people)); ensures r == c; { @@ -17,7 +28,7 @@ method FindCelebrity0(people: set, ghost c: Person) returns (r: r := cc; } -method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) requires IsCelebrity(c, people); ensures r == c; { @@ -40,7 +51,7 @@ method FindCelebrity1(people: set, ghost c: Person) returns (r: r := x; } -method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) requires IsCelebrity(c, people); ensures r == c; { @@ -64,7 +75,7 @@ method FindCelebrity2(people: set, ghost c: Person) returns (r: } r := b; } - +/* method FindCelebrity3(n: int, people: set, ghost c: int) returns (r: int) requires 0 < n; requires (forall p :: p in people <==> 0 <= p && p < n); @@ -88,3 +99,4 @@ method FindCelebrity3(n: int, people: set, ghost c: int) returns (r: int) } r := b; } +*/ \ No newline at end of file diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 39e14ea5..3387ea52 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -157,13 +157,14 @@ function last(xs: List): Nat case Cons(z, zs) => last(ys) } +/* function mapF(xs: List): List { match xs case Nil => Nil case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys)) } -function HardcodedUninterpretedFunction(n: Nat): Nat +function HardcodedUninterpretedFunction(n: Nat): Nat*/ function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List { @@ -186,7 +187,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List else Cons(y, ys) } -function filterP(xs: List): List +/*function filterP(xs: List): List { match xs case Nil => Nil @@ -195,7 +196,7 @@ function filterP(xs: List): List then Cons(y, filterP(ys)) else filterP(ys) } -function HardcodedUninterpretedPredicate(n: Nat): Bool +function HardcodedUninterpretedPredicate(n: Nat): Bool*/ function insort(n: Nat, xs: List): List { @@ -327,21 +328,22 @@ ghost method P11() { } +/* ghost method P12() ensures (forall n, xs :: drop(n, mapF(xs)) == mapF(drop(n, xs))); { -} +}*/ ghost method P13() ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs)); { } - +/* ghost method P14() ensures (forall xs, ys :: filterP(concat(xs, ys)) == concat(filterP(xs), filterP(ys))); { } - +*/ ghost method P15() ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs))); { @@ -478,12 +480,12 @@ ghost method P40() ensures (forall xs :: take(Zero, xs) == Nil); { } - +/* ghost method P41() ensures (forall n, xs :: take(n, mapF(xs)) == mapF(take(n, xs))); { } - +*/ ghost method P42() ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs))); { diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c8419890..0dfb6683 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -31,6 +31,9 @@ class UltraFilter { // Dafny currently does not have a set comprehension expression, so this method stub will have to do method H(f: set>, S: set, M: set) returns (h: set>) ensures (forall X :: X in h <==> M + X in f); + { + assume false; + } method Lemma_HIsFilter(h: set>, f: set>, S: set, M: set) requires IsFilter(f, S); -- cgit v1.2.3