From 0e2d86cd4fdfe917df8a6f755f4cccd66f2c16e2 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 19 Jun 2015 16:10:25 -0700 Subject: Fix various bugs in nested match patterns listed in issue #83 --- Test/dafny0/NestedPatterns.dfy | 124 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 124 insertions(+) create mode 100644 Test/dafny0/NestedPatterns.dfy (limited to 'Test/dafny0/NestedPatterns.dfy') diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy new file mode 100644 index 00000000..ef597936 --- /dev/null +++ b/Test/dafny0/NestedPatterns.dfy @@ -0,0 +1,124 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype List = Nil | Cons(head: T, tail: List) + +method MethodA(xs: List) returns (ys: List) +{ + match xs + case Nil => + ys := Nil; + case Cons(h, Nil) => + ys := Nil; + case Cons(h, Cons(h', tt)) => + ys := tt; +} + +method MethodB(xs: List) +{ + match xs + case Nil => + case Cons(h, Nil) => + var x := 12; + var xxs := Cons(Nil, Nil); + case Cons(h, Cons(h', tt)) => +} + +method MethodC(xs: List) returns (ys: List) + requires xs.Cons? ==> !xs.tail.Cons?; +{ + match xs + case Nil => + ys := Nil; + case Cons(h, Nil) => + ys := Nil; +} + +method MethodD(xs: List) returns (ys: List) +{ + match xs + case Nil => + ys := Nil; + case Cons(h, Nil) => + var xxs: List> := Cons(Nil, Nil); // BUG: type inference is not doing the right thing on this lint + case Cons(h, Cons(h0, tt)) => +} + +method MethodE(xs: List) returns (ys: List) +{ + var xxs: List> := Cons(Nil, Nil); // here it works! (but the same line in MethodD does not work) +} + +method MethodF(xs: List) returns (ys: List) + requires xs.Cons? ==> !xs.tail.Cons?; +{ + match xs + case Nil => + case Cons(h, Nil) => + case Cons(h0, Cons(h1, tt)) => // BUG: Dafny complains that Cons appears in more than one case; it seems to be due to the + // fact that the previous case uses identifier "h" as the first argument to Cons, whereas this + // line uses "h0" +} + +method MethodG(xs: List) returns (xxs: List>) +{ + match xs + case Nil => + xxs := Cons(Nil, Nil); // BUG: this causes there to be an "unresolved identifier: _mc#0" error; oddly enough, the error goes away if the third case is commented out + case Cons(h, t) => + case Cons(h, Cons(ht, tt)) => +} + +method AssertionFailure(xs: List) +{ + match xs + case (Nil) => // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here) + case (Cons(h, t)) => // BUG: ditto +} + +method DuplicateIdentifierInPattern0(xs: List) +{ + match xs + case Nil => + case Cons(h, Nil) => + case Cons(h, Cons(_, h)) => // BUG: this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported +} + +method DuplicateIdentifierInPattern1(xs: List) +{ + match xs + case Nil => + case Cons(h, Nil) => + case Cons(h, Cons(h, _)) => // BUG: this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported +} + +method DuplicateIdentifierInPattern2(xs: List) +{ + match xs + case Nil => + case Cons(h, Nil) => + case Cons(h, Cons(e, e)) => // BUG: here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal +} + +method Tuples0(xs: List, ys: List) +{ + match (xs, ys) + case (Nil, Nil) => + case (Cons(a, b), Nil) => + case (Nil, Cons(x, y)) => + case (Cons(a, b), Cons(x, y)) => // BUG: here and in some other places above, not all identifiers are highlighted in the Dafny IDE; it looks like + // only the identifiers in the last constructors are +} + +method Tuples1(xs: List, ys: List) +{ + match (xs, ys, 4) + case (Nil, Nil) => // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an + // assertion failure "mc.CasePatterns.Count == e.Arguments.Count" +} + +method Tuples2(xs: List, ys: List) +{ + match (xs, ys, ()) + case (Nil, Nil, ()) => // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1" +} -- cgit v1.2.3 From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 16:06:02 -0700 Subject: Type parameters in method/function signatures are no longer auto-declared. Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous. --- Source/Dafny/Resolver.cs | 6 ---- Test/dafny0/Basics.dfy | 2 +- Test/dafny0/Modules0.dfy | 14 ++++----- Test/dafny0/Modules0.dfy.expect | 19 +++--------- Test/dafny0/NestedMatch.dfy | 2 +- Test/dafny0/NestedPatterns.dfy | 8 ++--- Test/dafny0/ResolutionErrors.dfy | 10 +++--- Test/hofs/Examples.dfy | 14 ++++----- Test/hofs/Fold.dfy | 2 +- Test/hofs/Monads.dfy | 34 ++++++++++---------- Test/hofs/ReadsReads.dfy | 52 +++++++++++++++---------------- Test/hofs/ResolveError.dfy | 34 ++++++++++---------- Test/hofs/ResolveError.dfy.expect | 6 ++-- Test/hofs/Simple.dfy | 20 ++++++------ Test/hofs/TreeMapSimple.dfy | 24 +++++++-------- Test/hofs/Twice.dfy | 4 +-- Test/hofs/VectorUpdate.dfy | 65 +++++++++++++++++++++++++++++---------- Test/hofs/VectorUpdate.dfy.expect | 2 +- 18 files changed, 166 insertions(+), 152 deletions(-) (limited to 'Test/dafny0/NestedPatterns.dfy') diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 29e36ccd..7c78c1e2 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -8469,12 +8469,6 @@ namespace Microsoft.Dafny r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall); } #endif - } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && expr.OptTypeArguments == null) { - // it woulc plausibly be a type parameter, but isn't; we will declare it automatically - tp = new TypeParameter(expr.tok, expr.Name, defaultTypeArguments.Count, option.Parent); - defaultTypeArguments.Add(tp); - r = new Resolver_IdentifierExpr(expr.tok, tp); - allTypeParameters.Push(expr.Name, tp); } else { // ----- None of the above Error(expr.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", expr.Name); diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index c8fa76c8..89b0f02a 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -100,7 +100,7 @@ method ExpliesAssociativityM(A: bool, B: bool, C: bool) { } } -method ExpliesShortCircuiting(a: array) +method ExpliesShortCircuiting(a: array) { assert a == null || 0 <= a.Length; // (W) assert a != null ==> 0 <= a.Length; // (X) -- same as (W) diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 34aba3de..dbbffd87 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -71,16 +71,17 @@ module X1 { } module X2 { + import opened X1 class MyClass2 { - method Down(x1: MyClass1, x0: MyClass0) { + method Down(x1: MyClass1, x0: X0'.MyClass0) { x1.Down(x0); } - method WayDown(x0: MyClass0) { + method WayDown(x0: X0'.MyClass0) { x0.Down(); } method Up() { } - method Somewhere(y: MyClassY) { + method Somewhere(y: MyClassY) { // error: no such type in scope y.M(); } } @@ -97,8 +98,7 @@ module YY { class ClassG { method T() { } function method TFunc(): int { 10 } - method V(y: MyClassY) { // Note, MyClassY is in scope, since we are in the _default - // module, which imports everything + method V(y: MyClassY) { y.M(); } } @@ -141,10 +141,10 @@ class AClassWithSomeField { SomeField := SomeField + 4; var a := old(SomeField); // error: old can only be used in ghost contexts var b := fresh(this); // error: fresh can only be used in ghost contexts - var c := allocated(this); // error: allocated can only be used in ghost contexts +// var c := allocated(this); // error: allocated can only be used in ghost contexts if (fresh(this)) { // this guard makes the if statement a ghost statement ghost var x := old(SomeField); // this is a ghost context, so it's okay - ghost var y := allocated(this); // this is a ghost context, so it's okay +// ghost var y := allocated(this); // this is a ghost context, so it's okay } } } diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 5d11f9c9..d2f0bcc8 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -9,13 +9,8 @@ Modules0.dfy(15,11): Error: Duplicate name of top-level declaration: WazzupB Modules0.dfy(56,21): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?) Modules0.dfy(57,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) Modules0.dfy(68,21): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?) -Modules0.dfy(76,9): Error: type MyClass1 does not have a member Down -Modules0.dfy(76,13): Error: expected method call, found expression -Modules0.dfy(79,9): Error: type MyClass0 does not have a member Down -Modules0.dfy(79,13): Error: expected method call, found expression -Modules0.dfy(84,8): Error: type MyClassY does not have a member M -Modules0.dfy(84,9): Error: expected method call, found expression -Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?) +Modules0.dfy(84,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) +Modules0.dfy(93,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?) Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) Modules0.dfy(226,8): Error: new can be applied only to reference types (got X) Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X' @@ -35,11 +30,5 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon' Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List) Modules0.dfy(324,30): Error: member Create does not exist in class Klassy -Modules0.dfy(102,6): Error: type MyClassY does not have a member M -Modules0.dfy(102,7): Error: expected method call, found expression -Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts -Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts -Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts -Modules0.dfy(144,13): Error: unresolved identifier: allocated -Modules0.dfy(147,21): Error: unresolved identifier: allocated -42 resolution/type errors detected in Modules0.dfy +Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?) +31 resolution/type errors detected in Modules0.dfy diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy index e6e7c489..81319b4a 100644 --- a/Test/dafny0/NestedMatch.dfy +++ b/Test/dafny0/NestedMatch.dfy @@ -28,7 +28,7 @@ function last(xs: List): T case Cons(y, Cons(z, zs)) => last(Cons(z, zs)) } -method checkLast(y: T) { +method checkLast(y: T) { assert last(Cons(y, Nil)) == y; assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil)); } diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy index ef597936..d1d88b2a 100644 --- a/Test/dafny0/NestedPatterns.dfy +++ b/Test/dafny0/NestedPatterns.dfy @@ -69,7 +69,7 @@ method MethodG(xs: List) returns (xxs: List>) case Cons(h, Cons(ht, tt)) => } -method AssertionFailure(xs: List) +method AssertionFailure(xs: List) { match xs case (Nil) => // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here) @@ -100,7 +100,7 @@ method DuplicateIdentifierInPattern2(xs: List) case Cons(h, Cons(e, e)) => // BUG: here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal } -method Tuples0(xs: List, ys: List) +method Tuples0(xs: List, ys: List) { match (xs, ys) case (Nil, Nil) => @@ -110,14 +110,14 @@ method Tuples0(xs: List, ys: List) // only the identifiers in the last constructors are } -method Tuples1(xs: List, ys: List) +method Tuples1(xs: List, ys: List) { match (xs, ys, 4) case (Nil, Nil) => // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an // assertion failure "mc.CasePatterns.Count == e.Arguments.Count" } -method Tuples2(xs: List, ys: List) +method Tuples2(xs: List, ys: List) { match (xs, ys, ()) case (Nil, Nil, ()) => // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1" diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 761cffa0..8c910959 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1253,14 +1253,14 @@ module SignatureCompletion { datatype Dt = Ctor(X -> Dt) // error: X is not a declared type datatype Et = Ctor(X -> Et, Y) // error: X is not a declared type - // For methods and functions, signatures can auto-declare type parameters - method My0(s: set, x: A -> B) - method My1(x: A -> B, s: set) + + method My0(s: set, x: A -> B) + method My1(x: A -> B, s: set) method My2(s: set, x: A -> B) method My3(x: A -> B, s: set) - function F0(s: set, x: A -> B): int - function F1(x: A -> B, s: set): int + function F0(s: set, x: A -> B): int + function F1(x: A -> B, s: set): int function F2(s: set, x: A -> B): int function F3(x: A -> B, s: set): int } diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy index be2672f5..306d278d 100644 --- a/Test/hofs/Examples.dfy +++ b/Test/hofs/Examples.dfy @@ -1,14 +1,14 @@ // RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -function Apply(f: A -> B, x: A): B +function Apply(f: A -> B, x: A): B reads f.reads(x); requires f.requires(x); { f(x) } -function Apply'(f: A -> B) : A -> B +function Apply'(f: A -> B) : A -> B { x reads f.reads(x) requires f.requires(x) @@ -16,7 +16,7 @@ function Apply'(f: A -> B) : A -> B } -function Compose(f: B -> C, g:A -> B): A -> C +function Compose(f: B -> C, g:A -> B): A -> C { x reads g.reads(x) reads if g.requires(x) then f.reads(g(x)) else {} @@ -25,21 +25,21 @@ function Compose(f: B -> C, g:A -> B): A -> C => f(g(x)) } -function W(f : (A,A) -> A): A -> A +function W(f : (A,A) -> A): A -> A { x requires f.requires(x,x) reads f.reads(x,x) => f(x,x) } -function Curry(f : (A,B) -> C) : A -> B -> C +function Curry(f : (A,B) -> C) : A -> B -> C { x => y requires f.requires(x,y) reads f.reads(x,y) => f(x,y) } -function Uncurry(f : A -> B -> C) : (A,B) -> C +function Uncurry(f : A -> B -> C) : (A,B) -> C { (x,y) requires f.requires(x) requires f(x).requires(y) @@ -48,7 +48,7 @@ function Uncurry(f : A -> B -> C) : (A,B) -> C => f(x)(y) } -function S(f : (A,B) -> C, g : A -> B): A -> C +function S(f : (A,B) -> C, g : A -> B): A -> C { x requires g.requires(x) requires f.requires(x,g(x)) diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy index 6ca2d3b1..9bcd9e02 100644 --- a/Test/hofs/Fold.dfy +++ b/Test/hofs/Fold.dfy @@ -13,7 +13,7 @@ function method Eval(e : Expr): int case Lit(i) => i } -function method Fold(xs : List, unit : B, f : (A,B) -> B): B +function method Fold(xs : List, unit : B, f : (A,B) -> B): B reads f.reads; requires forall x, y :: x < xs ==> f.requires(x,y); { diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy index 3598d2b3..633dd339 100644 --- a/Test/hofs/Monads.dfy +++ b/Test/hofs/Monads.dfy @@ -4,29 +4,29 @@ abstract module Monad { type M - function method Return(x: A): M - function method Bind(m: M, f:A -> M):M - reads f.reads; - requires forall a :: f.requires(a); + function method Return(x: A): M + function method Bind(m: M, f:A -> M):M + reads f.reads + requires forall a :: f.requires(a) // return x >>= f = f x - lemma LeftIdentity(x : A, f : A -> M) - requires forall a :: f.requires(a); - ensures Bind(Return(x),f) == f(x); + lemma LeftIdentity(x : A, f : A -> M) + requires forall a :: f.requires(a) + ensures Bind(Return(x),f) == f(x) // m >>= return = m - lemma RightIdentity(m : M) - ensures Bind(m,Return) == m; + lemma RightIdentity(m : M) + ensures Bind(m,Return) == m // (m >>= f) >>= g = m >>= (x => f(x) >>= g) - lemma Associativity(m : M, f:A -> M, g: B -> M) - requires forall a :: f.requires(a); - requires forall b :: g.requires(b); + lemma Associativity(m : M, f:A -> M, g: B -> M) + requires forall a :: f.requires(a) + requires forall b :: g.requires(b) ensures Bind(Bind(m,f),g) == Bind(m,x reads f.reads(x) reads g.reads requires f.requires(x) - requires forall b :: g.requires(b) => Bind(f(x),g)); + requires forall b :: g.requires(b) => Bind(f(x),g)) } module Identity refines Monad { @@ -101,21 +101,21 @@ module List refines Monad { function method Return(x: A): M { Cons(x,Nil) } - function method Concat(xs: M, ys: M): M + function method Concat(xs: M, ys: M): M { match xs case Nil => ys case Cons(x,xs) => Cons(x,Concat(xs,ys)) } - function method Join(xss: M>) : M + function method Join(xss: M>) : M { match xss case Nil => Nil case Cons(xs,xss) => Concat(xs,Join(xss)) } - function method Map(xs: M, f: A -> B):M + function method Map(xs: M, f: A -> B):M reads f.reads; requires forall a :: f.requires(a); { @@ -170,7 +170,7 @@ module List refines Monad { ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs)); {} - lemma BindMorphism(xs : M, ys: M, f : A -> M) + lemma BindMorphism(xs : M, ys: M, f : A -> M) requires forall a :: f.requires(a); ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f)); { diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index e11473bd..a6f8d922 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -2,58 +2,58 @@ // RUN: %diff "%s.expect" "%t" module ReadsRequiresReads { - function MyReadsOk(f : A -> B, a : A) : set - reads f.reads(a); + function MyReadsOk(f : A -> B, a : A) : set + reads f.reads(a) { f.reads(a) } - function MyReadsOk2(f : A -> B, a : A) : set - reads f.reads(a); + function MyReadsOk2(f : A -> B, a : A) : set + reads f.reads(a) { (f.reads)(a) } - function MyReadsOk3(f : A -> B, a : A) : set - reads (f.reads)(a); + function MyReadsOk3(f : A -> B, a : A) : set + reads (f.reads)(a) { f.reads(a) } - function MyReadsOk4(f : A -> B, a : A) : set - reads (f.reads)(a); + function MyReadsOk4(f : A -> B, a : A) : set + reads (f.reads)(a) { (f.reads)(a) } - function MyReadsBad(f : A -> B, a : A) : set + function MyReadsBad(f : A -> B, a : A) : set { f.reads(a) // error: MyReadsBad does not have permission to read what f.reads(a) reads } - function MyReadsBad2(f : A -> B, a : A) : set + function MyReadsBad2(f : A -> B, a : A) : set { (f.reads)(a) // error: MyReadsBad2 does not have permission to read what f.reads(a) reads } - function MyReadsOk'(f : A -> B, a : A, o : object) : bool - reads f.reads(a); + function MyReadsOk'(f : A -> B, a : A, o : object) : bool + reads f.reads(a) { o in f.reads(a) } - function MyReadsBad'(f : A -> B, a : A, o : object) : bool + function MyReadsBad'(f : A -> B, a : A, o : object) : bool { o in f.reads(a) // error: MyReadsBad' does not have permission to read what f.reads(a) reads } - function MyRequiresOk(f : A -> B, a : A) : bool - reads f.reads(a); + function MyRequiresOk(f : A -> B, a : A) : bool + reads f.reads(a) { f.requires(a) } - function MyRequiresBad(f : A -> B, a : A) : bool + function MyRequiresBad(f : A -> B, a : A) : bool { f.requires(a) // error: MyRequiresBad does not have permission to read what f.requires(a) reads } @@ -72,11 +72,11 @@ module WhatWeKnowAboutReads { } class S { - var s : S; + var s : S } function ReadsSomething(s : S):() - reads s; + reads s {()} method MaybeSomething() { @@ -105,29 +105,29 @@ module WhatWeKnowAboutReads { module ReadsAll { function A(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o; - requires forall x :: f.requires(x); + reads set o,x | o in f.reads(x) :: o + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method B(f: int -> int) : int - reads set o,x | o in f.reads(x) :: o; - requires forall x :: f.requires(x); + reads set o,x | o in f.reads(x) :: o + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function C(f: int -> int) : int - reads f.reads; - requires forall x :: f.requires(x); + reads f.reads + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } function method D(f: int -> int) : int - reads f.reads; - requires forall x :: f.requires(x); + reads f.reads + requires forall x :: f.requires(x) { f(0) + f(1) + f(2) } diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy index 3c0d7cd9..ae838eb3 100644 --- a/Test/hofs/ResolveError.dfy +++ b/Test/hofs/ResolveError.dfy @@ -3,9 +3,9 @@ method ResolutionErrors() { - var x; - var g5 := x, y => (y, x); // fail at resolution - var g6 := x, (y => (y, x)); // fail at resolution + var x; + var g5 := x, y => (y, x); // fail at resolution + var g6 := x, (y => (y, x)); // fail at resolution } // cannot assign functions @@ -23,20 +23,20 @@ method Nope3() { method RequiresFail(f : int -> int) // ok - requires f(0) == 0; - requires f.requires(0); - requires f.reads(0) == {}; + requires f(0) == 0 + requires f.requires(0) + requires f.reads(0) == {} // fail - requires f(0) == true; - requires f(1,2) == 0; - requires f(true) == 0; - requires f.requires(true); - requires f.requires(1) == 0; - requires f.requires(1,2); - requires f.reads(true) == {}; - requires f.reads(1) == 0; - requires f.reads(1,2) == {}; + requires f(0) == true + requires f(1,2) == 0 + requires f(true) == 0 + requires f.requires(true) + requires f.requires(1) == 0 + requires f.requires(1,2) + requires f.reads(true) == {} + requires f.reads(1) == 0 + requires f.reads(1,2) == {} { } @@ -56,7 +56,7 @@ method Bla() { assert Bool; } -method Pli(f : A -> B) requires f != null; +method Pli(f : A -> B) requires f != null { var o : object; assert f != o; @@ -102,7 +102,7 @@ module AritySituations { w := V; // error } - method P(r: T -> U, x: T) returns (u: U) + method P(r: T -> U, x: T) returns (u: U) requires r.requires(x); { u := r(x); diff --git a/Test/hofs/ResolveError.dfy.expect b/Test/hofs/ResolveError.dfy.expect index c3e0c242..11471ffd 100644 --- a/Test/hofs/ResolveError.dfy.expect +++ b/Test/hofs/ResolveError.dfy.expect @@ -2,8 +2,8 @@ ResolveError.dfy(86,6): Error: RHS (of type ((int,bool)) -> real) not assignable ResolveError.dfy(91,15): Error: incorrect type of method in-parameter 0 (expected ? -> ?, got (int,bool) -> real) ResolveError.dfy(101,6): Error: RHS (of type (()) -> real) not assignable to LHS (of type () -> real) ResolveError.dfy(102,6): Error: RHS (of type () -> real) not assignable to LHS (of type (()) -> real) -ResolveError.dfy(7,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment -ResolveError.dfy(8,11): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(7,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment +ResolveError.dfy(8,9): Error: the number of left-hand sides (1) and right-hand sides (2) must match for a multi-assignment ResolveError.dfy(21,6): Error: LHS of assignment must denote a mutable field ResolveError.dfy(31,16): Error: arguments must have the same type (got int and bool) ResolveError.dfy(32,12): Error: wrong number of arguments to function application (function type 'int -> int' expects 1, got 2) @@ -17,7 +17,7 @@ ResolveError.dfy(39,18): Error: wrong number of arguments to function applicatio ResolveError.dfy(46,15): Error: a reads-clause expression must denote an object or a collection of objects (instead got int) ResolveError.dfy(47,7): Error: Precondition must be boolean (got int) ResolveError.dfy(56,9): Error: condition is expected to be of type bool, but is () -> bool -ResolveError.dfy(59,34): Error: arguments must have the same type (got A -> B and ?) +ResolveError.dfy(59,39): Error: arguments must have the same type (got A -> B and ?) ResolveError.dfy(62,11): Error: arguments must have the same type (got A -> B and object) ResolveError.dfy(68,24): Error: unresolved identifier: _ 22 resolution/type errors detected in ResolveError.dfy diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy index c27fa82c..6d98531e 100644 --- a/Test/hofs/Simple.dfy +++ b/Test/hofs/Simple.dfy @@ -50,7 +50,7 @@ method Main() { } function method succ(x : int) : int - requires x > 0; + requires x > 0 { x + 1 } @@ -74,24 +74,24 @@ method Main3() { } -function P(f: A -> B, x : A): B - reads (f.reads)(x); - requires (f.requires)(x); +function P(f: A -> B, x : A): B + reads (f.reads)(x) + requires (f.requires)(x) { f(x) } -function Q(f: U -> V, x : U): V - reads P.reads(f,x); - requires f.requires(x); // would be nice to be able to write P.requires(f,x) +function Q(f: U -> V, x : U): V + reads P.reads(f,x) + requires f.requires(x) // would be nice to be able to write P.requires(f,x) { P(f,x) } -function QQ(f: U -> V, x : U): V - reads ((() => ((()=>f)()).reads)())((()=>x)()); - requires ((() => ((()=>f)()).requires)())((()=>x)()); +function QQ(f: U -> V, x : U): V + reads ((() => ((()=>f)()).reads)())((()=>x)()) + requires ((() => ((()=>f)()).requires)())((()=>x)()) { ((() => P)())((()=>f)(),(()=>x)()) } diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy index a853b82c..6b8f1377 100644 --- a/Test/hofs/TreeMapSimple.dfy +++ b/Test/hofs/TreeMapSimple.dfy @@ -6,7 +6,7 @@ datatype List = Nil | Cons(head: A,tail: List) datatype Tree = Branch(val: A,trees: List>) function ListData(xs : List) : set - ensures forall x :: x in ListData(xs) ==> x < xs; + ensures forall x :: x in ListData(xs) ==> x < xs { match xs case Nil => {} @@ -14,32 +14,32 @@ function ListData(xs : List) : set } function TreeData(t0 : Tree) : set - ensures forall t :: t in TreeData(t0) ==> t < t0; + ensures forall t :: t in TreeData(t0) ==> t < t0 { var Branch(x,ts) := t0; {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y } -function Pre(f : A -> B, s : set) : bool - reads (set x, y | x in s && y in f.reads(x) :: y); +function Pre(f : A -> B, s : set) : bool + reads (set x, y | x in s && y in f.reads(x) :: y) { forall x :: x in s ==> f.reads(x) == {} && f.requires(x) } -function method Map(xs : List, f : A -> B): List - reads Pre.reads(f, ListData(xs)); - requires Pre(f, ListData(xs)); - decreases xs; +function method Map(xs : List, f : A -> B): List + reads Pre.reads(f, ListData(xs)) + requires Pre(f, ListData(xs)) + decreases xs { match xs case Nil => Nil case Cons(x,xs) => Cons(f(x),Map(xs,f)) } -function method TMap(t0 : Tree, f : A -> B) : Tree - reads Pre.reads(f, TreeData(t0)); - requires Pre(f, TreeData(t0)); - decreases t0; +function method TMap(t0 : Tree, f : A -> B) : Tree + reads Pre.reads(f, TreeData(t0)) + requires Pre(f, TreeData(t0)) + decreases t0 { var Branch(x,ts) := t0; Branch(f(x),Map(ts, t requires t in ListData(ts) diff --git a/Test/hofs/Twice.dfy b/Test/hofs/Twice.dfy index add7e83c..5d948a58 100644 --- a/Test/hofs/Twice.dfy +++ b/Test/hofs/Twice.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -function method Twice(f : A -> A): A -> A +function method Twice(f : A -> A): A -> A { x requires f.requires(x) && f.requires(f(x)) reads f.reads(x) reads if f.requires(x) then f.reads(f(x)) else {} @@ -29,7 +29,7 @@ method WithReads() { } -function method Twice_bad(f : A -> A): A -> A +function method Twice_bad(f : A -> A): A -> A { x requires f.requires(x) && f.requires(f(x)) reads f.reads(x) + f.reads(f(x)) diff --git a/Test/hofs/VectorUpdate.dfy b/Test/hofs/VectorUpdate.dfy index 96edbe77..ca6b20b3 100644 --- a/Test/hofs/VectorUpdate.dfy +++ b/Test/hofs/VectorUpdate.dfy @@ -1,28 +1,59 @@ // RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -method VectorUpdate(N: int, a : array, f : (int,A) -> A) - requires a != null; - requires N == a.Length; - requires forall j :: 0 <= j < N ==> f.requires(j,a[j]); - requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j]); - modifies a; - ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j])); +// this is a rather verbose version of the VectorUpdate method +method VectorUpdate(N: int, a : array, f : (int,A) -> A) + requires a != null + requires N == a.Length + requires forall j :: 0 <= j < N ==> f.requires(j,a[j]) + requires forall j :: 0 <= j < N ==> a !in f.reads(j,a[j]) + modifies a + ensures forall j :: 0 <= j < N ==> a[j] == f(j,old(a[j])) { var i := 0; - while (i < N) - invariant 0 <= i <= N; - invariant forall j :: i <= j < N ==> f.requires(j,a[j]); - invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j])); - invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j]); - invariant forall j :: i <= j < N ==> a[j] == old(a[j]); - invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j])); + while i < N + invariant 0 <= i <= N + invariant forall j :: i <= j < N ==> f.requires(j,a[j]) + invariant forall j :: 0 <= j < N ==> f.requires(j,old(a[j])) + invariant forall j :: i <= j < N ==> a !in f.reads(j,a[j]) + invariant forall j :: i <= j < N ==> a[j] == old(a[j]) + invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j])) { a[i] := f(i,a[i]); i := i + 1; } } +// here's a shorter version of the method above +method VectorUpdate'(a : array, f : (int,A) -> A) + requires a != null + requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j]) + modifies a + ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j])) +{ + var i := 0; + while i < a.Length + invariant 0 <= i <= a.Length + invariant forall j :: i <= j < a.Length ==> a[j] == old(a[j]) + invariant forall j :: 0 <= j < i ==> a[j] == f(j,old(a[j])) + { + a[i] := f(i,a[i]); + i := i + 1; + } +} + +// here's yet another version +method VectorUpdate''(a : array, f : (int,A) -> A) + requires a != null + requires forall j :: 0 <= j < a.Length ==> a !in f.reads(j,a[j]) && f.requires(j,a[j]) + modifies a + ensures forall j :: 0 <= j < a.Length ==> a[j] == f(j,old(a[j])) +{ + forall i | 0 <= i < a.Length { + a[i] := f(i,a[i]); + } +} + method Main() { var v := new int[10]; @@ -46,11 +77,11 @@ method Main() } method PrintArray(a : array) - requires a != null; + requires a != null { var i := 0; - while (i < a.Length) { - if (i != 0) { + while i < a.Length { + if i != 0 { print ", "; } print a[i]; diff --git a/Test/hofs/VectorUpdate.dfy.expect b/Test/hofs/VectorUpdate.dfy.expect index b01ace00..18a7b110 100644 --- a/Test/hofs/VectorUpdate.dfy.expect +++ b/Test/hofs/VectorUpdate.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 6 verified, 0 errors +Dafny program verifier finished with 10 verified, 0 errors Program compiled successfully Running... -- cgit v1.2.3