diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-08 12:54:11 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-08 12:54:11 -0800 |
| commit | 2dab50557b2584a82ffc7be8759d6a8a4720d1f9 (patch) | |
| tree | 90032dae0fc63feb8706519e6dd918441163eed0 /Test/dafny0/AutoReq.dfy | |
| parent | d6f192b7bb331d42a0a4dcd6ab125857a431ac67 (diff) | |
Add autoReq support for matches.
Add better handling of resolved data types in autoReq.
Diffstat (limited to 'Test/dafny0/AutoReq.dfy')
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 9e221900..00c74f50 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -222,7 +222,36 @@ module {:autoReq} M1 { }
}
-/* Not yet implemented
+module Datatypes {
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+
+ function f1(t:TheType):bool
+ requires t.TheType_builder? && t.x > 3;
+
+ function {:autoReq} test(t:TheType) : bool
+ {
+ f1(t)
+ }
+
+ function f2(x:int) : bool
+ requires forall t:TheType :: t.TheType_builder? && t.x > x;
+ {
+ true
+ }
+
+ // Should cause a function-requirement violation without autoReq
+ function f3(y:int) : bool
+ {
+ f2(y)
+ }
+
+ function {:autoReq} test2(z:int) : bool
+ {
+ f2(z)
+ }
+
+}
+
module Matches {
datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
@@ -236,6 +265,5 @@ module Matches { case TheType_copier(t) => true
}
}
-*/
|