diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | db6ef6c9e2bca859280cfbe17871c38da74977fc (patch) | |
| tree | d742312e6c9c69386f4c7111d9133ccc3d810e01 /Test/dafny0/TypeParameters.dfy | |
Initial set of files.
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy new file mode 100644 index 00000000..a5764be5 --- /dev/null +++ b/Test/dafny0/TypeParameters.dfy @@ -0,0 +1,22 @@ +class C<U> {
+ method M<T>(x: T, u: U) returns (y: T)
+ ensures x == y && u == u;
+ {
+ y := x;
+ }
+
+ function F<X>(x: X, u: U): bool
+ {
+ x == x && u == u
+ }
+
+ method Main(u: U)
+ {
+ var t := F(3,u) && F(this,u);
+ var kz;
+ call kz := M(t,u);
+ assert kz && (G() || !G());
+ }
+
+ function G<Y>(): Y;
+}
|