diff options
Diffstat (limited to 'Test/hofs')
-rw-r--r-- | Test/hofs/Examples.dfy | 14 | ||||
-rw-r--r-- | Test/hofs/Fold.dfy | 2 | ||||
-rw-r--r-- | Test/hofs/Monads.dfy | 34 | ||||
-rw-r--r-- | Test/hofs/ReadsReads.dfy | 52 | ||||
-rw-r--r-- | Test/hofs/ResolveError.dfy | 34 | ||||
-rw-r--r-- | Test/hofs/ResolveError.dfy.expect | 6 | ||||
-rw-r--r-- | Test/hofs/Simple.dfy | 20 | ||||
-rw-r--r-- | Test/hofs/TreeMapSimple.dfy | 24 | ||||
-rw-r--r-- | Test/hofs/Twice.dfy | 4 | ||||
-rw-r--r-- | Test/hofs/VectorUpdate.dfy | 65 | ||||
-rw-r--r-- | Test/hofs/VectorUpdate.dfy.expect | 2 |
11 files changed, 144 insertions, 113 deletions
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<A,B>(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'<A,B>(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<A,B,C>(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<A>(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<A,B,C>(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<A,B,C>(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<A,B,C>(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<A>, unit : B, f : (A,B) -> B): B +function method Fold<A,B>(xs : List<A>, 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<A> - function method Return(x: A): M<A> - function method Bind(m: M<A>, f:A -> M<B>):M<B> - reads f.reads; - requires forall a :: f.requires(a); + function method Return<A>(x: A): M<A> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + reads f.reads + requires forall a :: f.requires(a) // return x >>= f = f x - lemma LeftIdentity(x : A, f : A -> M<B>) - requires forall a :: f.requires(a); - ensures Bind(Return(x),f) == f(x); + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + requires forall a :: f.requires(a) + ensures Bind(Return(x),f) == f(x) // m >>= return = m - lemma RightIdentity(m : M<A>) - ensures Bind(m,Return) == m; + lemma RightIdentity<A>(m : M<A>) + ensures Bind(m,Return) == m // (m >>= f) >>= g = m >>= (x => f(x) >>= g) - lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>) - requires forall a :: f.requires(a); - requires forall b :: g.requires(b); + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + 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<A>(x: A): M<A> { Cons(x,Nil) } - function method Concat(xs: M<A>, ys: M<A>): M<A> + function method Concat<A>(xs: M<A>, ys: M<A>): M<A> { match xs case Nil => ys case Cons(x,xs) => Cons(x,Concat(xs,ys)) } - function method Join(xss: M<M<A>>) : M<A> + function method Join<A>(xss: M<M<A>>) : M<A> { match xss case Nil => Nil case Cons(xs,xss) => Concat(xs,Join(xss)) } - function method Map(xs: M<A>, f: A -> B):M<B> + function method Map<A,B>(xs: M<A>, f: A -> B):M<B> 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<A>, ys: M<A>, f : A -> M<B>) + lemma BindMorphism<A,B>(xs : M<A>, ys: M<A>, f : A -> M<B>) 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<object> - reads f.reads(a); + function MyReadsOk<A,B>(f : A -> B, a : A) : set<object> + reads f.reads(a) { f.reads(a) } - function MyReadsOk2(f : A -> B, a : A) : set<object> - reads f.reads(a); + function MyReadsOk2<A,B>(f : A -> B, a : A) : set<object> + reads f.reads(a) { (f.reads)(a) } - function MyReadsOk3(f : A -> B, a : A) : set<object> - reads (f.reads)(a); + function MyReadsOk3<A,B>(f : A -> B, a : A) : set<object> + reads (f.reads)(a) { f.reads(a) } - function MyReadsOk4(f : A -> B, a : A) : set<object> - reads (f.reads)(a); + function MyReadsOk4<A,B>(f : A -> B, a : A) : set<object> + reads (f.reads)(a) { (f.reads)(a) } - function MyReadsBad(f : A -> B, a : A) : set<object> + function MyReadsBad<A,B>(f : A -> B, a : A) : set<object> { f.reads(a) // error: MyReadsBad does not have permission to read what f.reads(a) reads } - function MyReadsBad2(f : A -> B, a : A) : set<object> + function MyReadsBad2<A,B>(f : A -> B, a : A) : set<object> { (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'<A,B>(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'<A,B>(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<A,B>(f : A -> B, a : A) : bool + reads f.reads(a) { f.requires(a) } - function MyRequiresBad(f : A -> B, a : A) : bool + function MyRequiresBad<A,B>(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<A,B>(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<T,U>(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<A,B>(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<U,V>(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<U,V>(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<A> = Nil | Cons(head: A,tail: List<A>) datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>) 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<A>) : bool - reads (set x, y | x in s && y in f.reads(x) :: y); +function Pre<A,B>(f : A -> B, s : set<A>) : 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<A>, f : A -> B): List<B> - reads Pre.reads(f, ListData(xs)); - requires Pre(f, ListData(xs)); - decreases xs; +function method Map<A,B>(xs : List<A>, f : A -> B): List<B> + 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<A>, f : A -> B) : Tree<B> - reads Pre.reads(f, TreeData(t0)); - requires Pre(f, TreeData(t0)); - decreases t0; +function method TMap<A,B>(t0 : Tree<A>, f : A -> B) : Tree<B> + 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<A>(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<A>(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<A>, 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<A>(N: int, a : array<A>, 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>(a : array<A>, 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>(a : array<A>, 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<int>) - 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...
|