diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 42 | ||||
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 288 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
3 files changed, 331 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7da30e96..364e6c93 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2043,6 +2043,48 @@ Dafny program verifier finished with 3 verified, 3 errors Dafny program verifier finished with 2 verified, 0 errors
+-------------------- AutoReq.dfy --------------------
+AutoReq.dfy(245,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(11,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(23,3): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+AutoReq.dfy(36,12): Error: assertion violation
+AutoReq.dfy(29,13): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+AutoReq.dfy(36,12): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+AutoReq.dfy(38,12): Error: assertion violation
+AutoReq.dfy(29,27): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+AutoReq.dfy(38,12): Error: possible violation of function precondition
+Execution trace:
+ (0,0): anon0
+ (0,0): anon10_Then
+AutoReq.dfy(43,12): Error: assertion violation
+AutoReq.dfy(29,13): Related location
+AutoReq.dfy(5,5): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+
+Dafny program verifier finished with 46 verified, 8 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy new file mode 100644 index 00000000..684de262 --- /dev/null +++ b/Test/dafny0/AutoReq.dfy @@ -0,0 +1,288 @@ +
+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)
+ }
+ }
+}
+
+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);
+
+ 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
+ }
+}
+
+// Make sure :autoReq works with static functions
+module StaticTest {
+ static function f(x:int) : bool
+ requires x > 3;
+ {
+ x > 7
+ }
+
+ static function {:autoReq} g(z:int) : bool
+ requires f(z);
+ {
+ true
+ }
+
+ // Should succeed thanks to auto-generation based on f's requirements
+ static function {:autoReq} h(y:int) : bool
+ {
+ g(y)
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index ae80dc89..3d4af611 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -29,7 +29,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy IteratorResolution.dfy Iterators.dfy
RankPos.dfy RankNeg.dfy
Computations.dfy ComputationsNeg.dfy
- Include.dfy) do (
+ Include.dfy AutoReq.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|