summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-01-23 16:24:54 -0800
committerGravatar Rustan Leino <unknown>2013-01-23 16:24:54 -0800
commita5ba9b840d5fa93fb1841edfe74cddf2d259087d (patch)
tree759691bdd6b07c6a2e021b9eaa5de50c4af03d47 /Test/dafny0
parent75dc25ca53d1be853555064ae010e80ef7dd54b7 (diff)
Split verification of quantifier expressions into #2 for checked and #1 for assumed.
Fixed cases where token was not being updated for refinement.
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Answer5
-rw-r--r--Test/dafny0/Predicates.dfy46
-rw-r--r--Test/dafny0/SplitExpr.dfy19
3 files changed, 46 insertions, 24 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 85d8c977..e3e513a4 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1397,6 +1397,7 @@ Execution trace:
(0,0): anon9_Then
(0,0): anon10_Then
CoPrefix.dfy(139,25): Error: assertion violation
+CoPrefix.dfy(114,23): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon9_Then
@@ -1448,11 +1449,13 @@ Execution trace:
(0,0): anon3_Then
CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -1506,7 +1509,7 @@ EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must sup
-------------------- SplitExpr.dfy --------------------
-Dafny program verifier finished with 5 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
-------------------- LoopModifies.dfy --------------------
LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 19375ac2..1610d8b8 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -15,7 +15,7 @@ module A {
method N()
modifies this;
ensures P();
- {
+ { // error: in module B, the postcondition P() has been strengthened and no longer holds
x := -28;
}
}
@@ -36,7 +36,7 @@ module Loose {
class MyNumber {
var N: int;
ghost var Repr: set<object>;
- predicate Valid
+ predicate Valid()
reads this, Repr;
{
this in Repr && null !in Repr &&
@@ -44,20 +44,20 @@ module Loose {
}
constructor Init()
modifies this;
- ensures Valid && fresh(Repr - {this});
+ ensures Valid() && fresh(Repr - {this});
{
N, Repr := 0, {this};
}
method Inc()
- requires Valid;
+ requires Valid();
modifies Repr;
ensures old(N) < N;
- ensures Valid && fresh(Repr - old(Repr));
+ ensures Valid() && fresh(Repr - old(Repr));
{
N := N + 2;
}
method Get() returns (n: int)
- requires Valid;
+ requires Valid();
ensures n == N;
{
n := N;
@@ -67,7 +67,7 @@ module Loose {
module Tight refines Loose {
class MyNumber {
- predicate Valid
+ predicate Valid()
{
N % 2 == 0
}
@@ -107,20 +107,20 @@ module AwareClient {
module Tricky_Base {
class Tree {
var x: int;
- predicate Constrained
+ predicate Constrained()
reads this;
{
x < 10
}
- predicate Valid
+ predicate Valid()
reads this;
{
x < 100
}
method Init()
modifies this;
- ensures Valid;
- {
+ ensures Valid();
+ { // error: in module Tricky_Full, the strengthened postcondition Valid() no longer holds
x := 20;
}
}
@@ -128,7 +128,7 @@ module Tricky_Base {
module Tricky_Full refines Tricky_Base {
class Tree {
- predicate Valid
+ predicate Valid()
{
Constrained // this causes an error to be generated for the inherited Init
}
@@ -140,43 +140,43 @@ module Tricky_Full refines Tricky_Base {
module Q0 {
class C {
var x: int;
- predicate P
+ predicate P()
reads this;
{
true
}
method M()
modifies this;
- ensures forall c: C :: c != null ==> c.P;
- {
+ ensures forall c: C :: c != null ==> c.P();
+ { // error: in module Q1, the postcondition no longer holds
}
- predicate Q
+ predicate Q()
reads this;
{
x < 100
}
method N()
modifies this;
- ensures forall c :: c == this ==> c.Q;
- {
- x := 102; // error: fails to establish postcondition (but this error should not be repeated in Q1 below)
+ ensures forall c :: c == this ==> c.Q();
+ { // error: fails to establish postcondition (but this error should not be repeated in Q1 below)
+ x := 102;
}
- predicate R reads this; // a body-less predicate
+ predicate R() reads this; // a body-less predicate
}
}
module Q1 refines Q0 {
class C {
- predicate P
+ predicate P()
{
x == 18
}
- predicate R // no body yet
+ predicate R() // no body yet
}
}
module Q2 refines Q1 {
class C {
- predicate R { x % 3 == 2 } // finally, give it a body
+ predicate R() { x % 3 == 2 } // finally, give it a body
}
}
diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy
index 80b67c10..3e67db58 100644
--- a/Test/dafny0/SplitExpr.dfy
+++ b/Test/dafny0/SplitExpr.dfy
@@ -54,3 +54,22 @@ class Node<T> {
next.Valid())
}
}
+
+// ---------------------------------------------------------------------------------------
+// The following examples requires that quantifiers are boosted (that is, #2) when checked
+// versus not boosted (#1) when assumed.
+
+function F(x: nat): int
+{
+ if x == 0 then 0 else 1 + F(x-1)
+}
+
+method M(N: nat)
+{
+ var i := 0;
+ while (i < N)
+ invariant forall x {:induction false} :: 0 <= x <= i ==> F(x) == x;
+ {
+ i := i + 1;
+ }
+}