From 724cd08bb69546967483e13fdd1a7c7b9797f59b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sun, 20 Jan 2013 14:02:09 -0800 Subject: Added some co- test cases. Fixed some bugs. --- Test/dafny0/Answer | 16 +++++- Test/dafny0/CoPrefix.dfy | 41 ++++++++++++++ Test/dafny3/Answer | 8 +++ Test/dafny3/CalcExample.dfy | 27 +++++++++ Test/dafny3/SimpleCoinduction.dfy | 115 ++++++++++++++++++++++++++++++++++++++ Test/dafny3/runtest.bat | 5 +- 6 files changed, 210 insertions(+), 2 deletions(-) create mode 100644 Test/dafny3/CalcExample.dfy create mode 100644 Test/dafny3/SimpleCoinduction.dfy (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 760e6880..13e7a8b0 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1336,6 +1336,20 @@ CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to o 10 resolution/type errors detected in CoResolution.dfy -------------------- CoPrefix.dfy -------------------- +CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path. +CoPrefix.dfy(160,15): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +CoPrefix.dfy(166,3): Error BP5003: A postcondition might not hold on this return path. +CoPrefix.dfy(165,15): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +CoPrefix.dfy(173,5): Error: cannot prove termination; try supplying a decreases clause +Execution trace: + (0,0): anon0 + (0,0): anon3_Then CoPrefix.dfy(60,7): Error: failure to decrease termination measure Execution trace: (0,0): anon0 @@ -1370,7 +1384,7 @@ Execution trace: (0,0): anon0 (0,0): anon3_Else -Dafny program verifier finished with 24 verified, 6 errors +Dafny program verifier finished with 41 verified, 9 errors -------------------- CoinductiveProofs.dfy -------------------- CoinductiveProofs.dfy(26,12): Error: assertion violation diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index 991e160f..d3cecc28 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -148,3 +148,44 @@ comethod {:induction false} BadTheorem(s: IList) { // error: postcondition violation BadTheorem(s.tail); } + +// --------------------------------- + +// Make sure recursive calls get checked for termination +module Recursion { + comethod X() { Y(); } + comethod Y() { X(); } + + comethod G(x: int) + ensures x < 100; + { // error: postcondition violation (when _k == 0) + H(x); + } + comethod H(x: int) + ensures x < 100; + { // error: postcondition violation (when _k == 0) + G(x); + } + + comethod A(x: int) { B(x); } + comethod B(x: int) + { + A#[10](x); // error: this is a recursive call, and the termination metric may not be going down + } + + comethod A'(x: int) { B'(x); } + comethod B'(x: int) + { + if (10 < _k) { + A'#[10](x); + } + } + + comethod A''(x: int) { B''(x); } + comethod B''(x: int) + { + if (0 < x) { + A''#[_k](x-1); + } + } +} diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index 9cd8fc82..c4e75986 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -14,3 +14,11 @@ Dafny program verifier finished with 11 verified, 0 errors -------------------- CachedContainer.dfy -------------------- Dafny program verifier finished with 47 verified, 0 errors + +-------------------- SimpleCoinduction.dfy -------------------- + +Dafny program verifier finished with 28 verified, 0 errors + +-------------------- CalcExample.dfy -------------------- + +Dafny program verifier finished with 6 verified, 0 errors diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy new file mode 100644 index 00000000..c94c18d2 --- /dev/null +++ b/Test/dafny3/CalcExample.dfy @@ -0,0 +1,27 @@ +function f(x: int, y: int): int + +ghost method Associativity(x: int, y: int, z: int) + ensures f(x, f(y, z)) == f(f(x, y), z); + +ghost method Monotonicity(y: int, z: int) + requires y <= z; + ensures forall x :: f(x, y) <= f(x, z); + +ghost method DiagonalIdentity(x: int) + ensures f(x, x) == x; + +method M(a: int, b: int, c: int, x: int) + requires c <= x == f(a, b); +{ + calc { + f(a, f(b, c)); + { Associativity(a, b, c); } + f(f(a, b), c); + { assert f(a, b) == x; } + f(x, c); + { assert c <= x; Monotonicity(c, x); } + <= f(x, x); + { DiagonalIdentity(x); } + x; + } +} diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy new file mode 100644 index 00000000..5a8ab288 --- /dev/null +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -0,0 +1,115 @@ +codatatype Stream = Cons(head: T, tail: Stream); +codatatype IList = Nil | ICons(head: T, tail: IList); + +// ----------------------------------------------------------------------- + +copredicate Pos(s: Stream) +{ + s.head > 0 && Pos(s.tail) +} + +function Up(n: int): Stream +{ + Cons(n, Up(n+1)) +} + +function Inc(s: Stream): Stream +{ + Cons(s.head + 1, Inc(s.tail)) +} + +ghost method {:induction false} UpLemma(k: nat, n: int) + ensures Inc(Up(n)) ==#[k] Up(n+1); +{ + if (k != 0) { + UpLemma(k-1, n+1); + } +} + +comethod {:induction false} CoUpLemma(n: int) + ensures Inc(Up(n)) == Up(n+1); +{ + CoUpLemma(n+1); +} + +ghost method UpLemma_Auto(k: nat, n: int) + ensures Inc(Up(n)) ==#[k] Up(n+1); +{ +} + +comethod CoUpLemma_Auto(n: int) + ensures Inc(Up(n)) == Up(n+1); +{ +} + +// ----------------------------------------------------------------------- + +function Repeat(n: int): Stream +{ + Cons(n, Repeat(n)) +} + +comethod RepeatLemma(n: int) + ensures Inc(Repeat(n)) == Repeat(n+1); +{ +} + +// ----------------------------------------------------------------------- + +copredicate True(s: Stream) +{ + True(s.tail) +} + +comethod AlwaysTrue(s: Stream) + ensures True(s); +{ + AlwaysTrue(s.tail); // WHY does this not happen automatically? (Because 's' is not quantified over) +} + +copredicate AlsoTrue(s: Stream) +{ + AlsoTrue(s) +} + +comethod AlsoAlwaysTrue(s: Stream) + ensures AlsoTrue(s); +{ + // AlsoAlwaysTrue(s); // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over +} + +// ----------------------------------------------------------------------- + +function Append(M: IList, N: IList): IList +{ + match M + case Nil => N + case ICons(x, M') => ICons(x, Append(M', N)) +} + +function zeros(): IList +{ + ICons(0, zeros()) +} + +function ones(): IList +{ + ICons(1, ones()) +} + +copredicate AtMost(a: IList, b: IList) +{ + match a + case Nil => true + case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail) +} + +comethod ZerosAndOnes_Theorem0() + ensures AtMost(zeros(), ones()); +{ +} + +comethod ZerosAndOnes_Theorem1() + ensures Append(zeros(), ones()) == zeros(); +{ +} diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index 2ebba74a..83d2bba9 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -4,7 +4,10 @@ setlocal set BINARIES=..\..\Binaries set DAFNY_EXE=%BINARIES%\Dafny.exe -for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy) do ( +for %%f in ( + Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy + SimpleCoinduction.dfy CalcExample.dfy +) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -- cgit v1.2.3