diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-08 09:39:21 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-08 09:39:21 -0800 |
| commit | d6f192b7bb331d42a0a4dcd6ab125857a431ac67 (patch) | |
| tree | df31e9a272a72c643da3e359097dbb1b3277b4a2 /Test/dafny0/AutoReq.dfy | |
| parent | 4ebde4044d39a93fd3178b8cb688eb57cd52ffa8 (diff) | |
Added support for automatic generation of function requirements via the :autoReq attribute.
Diffstat (limited to 'Test/dafny0/AutoReq.dfy')
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 241 |
1 files changed, 241 insertions, 0 deletions
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy new file mode 100644 index 00000000..9e221900 --- /dev/null +++ b/Test/dafny0/AutoReq.dfy @@ -0,0 +1,241 @@ +
+function f(x:int) : bool
+ requires x > 3;
+{
+ x > 7
+}
+
+// Should cause a function-requires failure
+function g(y:int) : bool
+{
+ f(y)
+}
+
+// Should succeed thanks to auto-generation based on f's requirements
+function {:autoReq} h(y:int) : bool
+{
+ f(y)
+}
+
+// Should fail based on h's inferred requirements
+function h_tester() : bool
+{
+ h(2)
+}
+
+// Should succeed thanks to auto_reqs
+function {:autoReq} i(y:int, b:bool) : bool
+{
+ if b then f(y + 2) else f(2*y)
+}
+
+method test()
+{
+ // Function req violations (and assertion violations)
+ if (*) {
+ assert i(1, true);
+ } else if (*) {
+ assert i(0, false);
+ }
+
+ // Make sure function i's reqs can be satisfied
+ if (*) {
+ assert i(3, true); // False assertion
+ }
+ assert i(7, false); // True assertion
+}
+
+module {:autoReq} TwoLayersOfRequires {
+ function f(x:int) : bool
+ requires x > 4;
+ {
+ x > 5
+ }
+
+ function g(y:int) : bool
+ requires y < 50;
+ {
+ f(y)
+ }
+
+ function h(z:int) : bool
+ {
+ g(z)
+ }
+}
+
+module {:autoReq} QuantifierTestsSimple {
+ function byte(x:int) : bool
+ {
+ 0 <= x < 256
+ }
+
+ function f_forall(s:seq<int>) : bool
+ {
+ forall i :: 0 <= i < |s| ==> byte(s[i])
+ }
+
+ function f_exists(s:seq<int>) : bool
+ {
+ exists i :: 0 <= i < |s| && byte(s[i])
+ }
+
+ function g_forall(s:seq<int>) : bool
+ requires f_forall(s);
+ {
+ |s| > 2
+ }
+
+ function g_exists(s:seq<int>) : bool
+ requires f_exists(s);
+ {
+ |s| > 2
+ }
+
+ function h(s:seq<int>) : bool
+ {
+ g_forall(s) && g_exists(s)
+ }
+}
+
+module {:autoReq} QuantifierTestsHard {
+ function byte(x:int) : bool
+ requires 0 <= x < 256;
+ { true }
+
+ function f_forall(s:seq<int>) : bool
+ {
+ forall i :: 0 <= i < |s| ==> byte(s[i])
+ }
+
+ function f_exists(s:seq<int>) : bool
+ {
+ exists i :: 0 <= i < |s| && byte(s[i])
+ }
+
+ function g_forall(s:seq<int>) : bool
+ requires forall j :: 0 <= j < |s| ==> byte(s[j]);
+ {
+ |s| > 2
+ }
+
+ function h_forall(s:seq<int>) : bool
+ {
+ f_forall(s)
+ }
+
+ function h(s:seq<int>) : bool
+ {
+ g_forall(s)
+ }
+
+ function i(s:seq<int>) : bool
+ requires forall k :: 0 <= k < |s| ==> 0 <= s[k] < 5;
+ {
+ true
+ }
+
+ function j(s:seq<int>) : bool
+ {
+ i(s)
+ }
+
+ function m(x:int) : bool
+ function n(x:int) : bool
+
+ function f1(x:int) : bool
+ requires x > 3;
+ requires x < 16;
+
+ function variable_uniqueness_test(x:int) : bool
+ {
+ (forall y:int :: m(y))
+ &&
+ f1(x)
+ }
+}
+
+module CorrectReqOrdering {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function f2(b:bool) : bool
+ requires b;
+
+ // Should pass if done correctly.
+ // However, if Dafny incorrectly put the requires for f2 first,
+ // then the requires for f1 won't be satisfied
+ function {:autoReq} f3(z:int) : bool
+ {
+ f2(f1(z))
+ }
+
+}
+
+module ShortCircuiting {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function f2(y:int) : bool
+ requires y < 10;
+
+ function {:autoReq} test1(x':int, y':int) : bool
+ {
+ f1(x') && f2(y')
+ }
+
+ function {:autoReq} test2(x':int, y':int) : bool
+ {
+ f1(x') ==> f2(y')
+ }
+
+ function {:autoReq} test3(x':int, y':int) : bool
+ {
+ f1(x') || f2(y')
+ }
+}
+
+module Lets {
+ function f1(x:int) : bool
+ requires x > 3;
+
+ function {:autoReq} test1(x':int) : bool
+ {
+ var y' := 3*x'; f1(y')
+ }
+}
+
+// Test nested module specification of :autoReq attribute
+module {:autoReq} M1 {
+ module M2 {
+ function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ function {:autoReq} h(y:int) : bool
+ {
+ f(y)
+ }
+ }
+}
+
+/* Not yet implemented
+module Matches {
+ datatype TheType = TheType_builder(x:int) | TheType_copier(t:TheType);
+
+ function f1(x:int):bool
+ requires x > 3;
+
+ function {:autoReq} basic_test(t:TheType) : bool
+ {
+ match t
+ case TheType_builder(x) => f1(x)
+ case TheType_copier(t) => true
+ }
+}
+*/
+
+
|