diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 24 | ||||
| -rw-r--r-- | Test/dafny0/RankNeg.dfy | 31 | ||||
| -rw-r--r-- | Test/dafny0/RankPos.dfy | 79 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArrayAuto.dfy | 2 | ||||
| -rw-r--r-- | Test/vstte2012/RingBufferAuto.dfy | 2 |
7 files changed, 140 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index dd5e620f..97097cfd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1671,6 +1671,30 @@ Execution trace: Dafny program verifier finished with 38 verified, 11 errors
+-------------------- RankPos.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
+
+-------------------- RankNeg.dfy --------------------
+RankNeg.dfy(7,26): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+RankNeg.dfy(12,28): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+RankNeg.dfy(19,31): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+RankNeg.dfy(29,25): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+
+Dafny program verifier finished with 1 verified, 4 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/RankNeg.dfy b/Test/dafny0/RankNeg.dfy new file mode 100644 index 00000000..39e7630d --- /dev/null +++ b/Test/dafny0/RankNeg.dfy @@ -0,0 +1,31 @@ +// Negative tests
+
+// Not well-founded mutual recursions.
+
+function seq_loop_i(xs: seq<int>): int
+{
+ if (xs == [1, 2]) then seq_loop_s([[1,2]])
+ else 0
+}
+function seq_loop_s(xs: seq<seq<int>>): int
+{
+ if (xs == [[1, 2]]) then seq_loop_i([1,2])
+ else 0
+}
+
+datatype wrap = X | WS(ds: seq<wrap>);
+function wrap_loop_1(xs: seq<wrap>): int
+{
+ if (xs == [WS([X,X])]) then wrap_loop_2(WS([X,X]))
+ else 0
+}
+function wrap_loop_2(xs: wrap): int
+{
+ if (xs == WS([X,X])) then wrap_loop_3([X,X])
+ else 0
+}
+function wrap_loop_3(xs: seq<wrap>): int
+{
+ if (xs == [X,X]) then wrap_loop_1([WS([X,X])])
+ else 0
+}
diff --git a/Test/dafny0/RankPos.dfy b/Test/dafny0/RankPos.dfy new file mode 100644 index 00000000..bc48a6c8 --- /dev/null +++ b/Test/dafny0/RankPos.dfy @@ -0,0 +1,79 @@ +datatype list<A> = Nil | Cons(head: A, tail: list<A>);
+datatype d = A | B(ds: list<d>);
+datatype d2 = A2 | B2(ds: seq<d2>);
+datatype d3 = A3 | B3(ds: set<d3>);
+
+function d_size(x: d): int
+{
+ match x
+ case A => 1
+ case B(ds) => 1+ds_size(ds)
+}
+
+function ds_size(xs: list<d>): int
+{
+ match xs
+ case Nil => 1
+ case Cons(head, tail) => d_size(head)+ds_size(tail)
+}
+
+function d2_size(x: d2): int
+{
+ match x
+ case A2 => 1
+ case B2(ds) => 1+ds2_size(ds)
+}
+
+function ds2_size(xs: seq<d2>): int
+{
+ if (|xs|==0) then 1 else 1+d2_size(xs[0])+ds2_size(xs[1..])
+}
+
+function seq_dec_drop(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ 1+seq_dec_drop(xs[1..])
+}
+
+function seq_dec_take(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ 1+seq_dec_take(xs[..|xs|-1])
+}
+
+function seq_dec(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ var i :| 0 < i <= |xs|;
+ i+seq_dec(xs[i..])
+}
+
+function seq_dec'(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ var i :| 0 <= i < |xs|;
+ i+seq_dec'(xs[..i])
+}
+
+function seq_dec''(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ var i :| 0 <= i < |xs|;
+ assert xs[0..i] == xs[..i];
+ i+seq_dec''(xs[0..i])
+}
+
+function seq_dec'''(xs: seq<int>): int
+ decreases |xs|;
+{
+ if (|xs|==0) then 0 else
+ var i :| 0 <= i < |xs|;
+ i+seq_dec'''(xs[..i]+xs[i+1..])
+}
+
+function seq_dec''''(xs: seq<int>): int
+{
+ if (|xs|==0) then 0 else
+ var i :| 0 <= i < |xs|;
+ i+seq_dec''''(xs[..i]+xs[i+1..])
+}
\ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 1bb2ef9f..c238b1f4 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -25,7 +25,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
+ Calculations.dfy IteratorResolution.dfy Iterators.dfy
+ RankPos.dfy RankNeg.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index adf97863..57ac69c7 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -83,7 +83,7 @@ class ExtensibleArray<T> { modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + [t];
- decreases Contents;
+ decreases |Contents|;
{
if (length == 0 || length % 256 != 0) {
// there is room in "elements"
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy index a3c5593c..b05af9f9 100644 --- a/Test/dafny1/ExtensibleArrayAuto.dfy +++ b/Test/dafny1/ExtensibleArrayAuto.dfy @@ -70,7 +70,7 @@ class {:autocontracts} ExtensibleArray<T> { method Append(t: T)
ensures Contents == old(Contents) + [t];
- decreases Contents;
+ decreases |Contents|;
{
if (length == 0 || length % 256 != 0) {
// there is room in "elements"
diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy index f51a36b2..7ce48fcc 100644 --- a/Test/vstte2012/RingBufferAuto.dfy +++ b/Test/vstte2012/RingBufferAuto.dfy @@ -55,6 +55,8 @@ class {:autocontracts} RingBuffer<T> method Dequeue() returns (x: T)
requires Contents != [];
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
{
x := data[start];
|