diff options
Diffstat (limited to 'Test')
46 files changed, 843 insertions, 794 deletions
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 23c25733..274d86de 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -49,7 +49,7 @@ method M(N: int, A: array<int>, B: array<int>) assert forall j,k :: 0 <= j < k < N ==> B[j] != B[k];
}
-static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
+function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
method Main()
{
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy index 61bb2e3a..814e9067 100644 --- a/Test/VSComp2010/Problem3-FindZero.dfy +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -56,7 +56,7 @@ class Node { }
}
-static method Search(ll: Node) returns (r: int)
+method Search(ll: Node) returns (r: int)
requires ll == null || ll.Valid();
ensures ll == null ==> r == 0;
ensures ll != null ==>
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 21fcc053..487dfdf2 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -47,7 +47,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) // Given a board, this function says whether or not the queen placed in column 'pos'
// is consistent with the queens placed in columns to its left.
-static function method IsConsistent(board: seq<int>, pos: int): bool
+function method IsConsistent(board: seq<int>, pos: int): bool
{
0 <= pos && pos < |board| &&
(forall q :: 0 <= q && q < pos ==>
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 9e0d3b63..99e8298e 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -270,44 +270,44 @@ module Matches { // Make sure :autoReq works with static functions
module StaticTest {
- static function f(x:int) : bool
+ function f(x:int) : bool
requires x > 3;
{
x > 7
}
- static function {:autoReq} g(z:int) : bool
+ 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
+ function {:autoReq} h(y:int) : bool
{
g(y)
}
- static predicate IsEven(x:int)
+ predicate IsEven(x:int)
- static function EvenDoubler(x:int) : int
+ function EvenDoubler(x:int) : int
requires IsEven(x);
// Should succeed thanks to auto-generated requirement of IsEven
- static function {:autoReq} test(y:int) : int
+ function {:autoReq} test(y:int) : int
{
EvenDoubler(y)
}
}
module OpaqueTest {
- static function bar(x:int) : int
+ function bar(x:int) : int
requires x>7;
{
x-2
}
- static function {:autoReq} {:opaque} foo(x:int) : int
+ function {:autoReq} {:opaque} foo(x:int) : int
{
bar(x)
}
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 57a593fe..dfa99dd6 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -2,32 +2,34 @@ // RUN: %diff "%s.expect" "%t"
module TestModule {
- copredicate P(b: bool)
- {
- !b && Q(null)
- }
+ class TestClass {
+ copredicate P(b: bool)
+ {
+ !b && Q(null)
+ }
- copredicate Q(a: array<int>)
- {
- a == null && P(true)
- }
+ copredicate Q(a: array<int>)
+ {
+ a == null && P(true)
+ }
- copredicate S(d: set<int>)
- {
- this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- this.S#[5](d) &&
- S#[5](d) &&
- S#[_k](d) // error: _k is not an identifier in scope
- }
+ copredicate S(d: set<int>)
+ {
+ this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ this.S#[5](d) &&
+ S#[5](d) &&
+ S#[_k](d) // error: _k is not an identifier in scope
+ }
- colemma CM(d: set<int>)
- {
- var b;
- b := this.S#[5](d);
- b := S#[5](d);
- this.CM#[5](d);
- CM#[5](d);
+ colemma CM(d: set<int>)
+ {
+ var b;
+ b := this.S#[5](d);
+ b := S#[5](d);
+ this.CM#[5](d);
+ CM#[5](d);
+ }
}
}
@@ -63,19 +65,21 @@ module GhostCheck2 { }
module Mojul0 {
- copredicate D()
- reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
- {
- true
- }
+ class MyClass {
+ copredicate D()
+ reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
+ {
+ true
+ }
- copredicate NoEnsuresPlease(m: nat)
- ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
- {
- m < 75
- }
+ copredicate NoEnsuresPlease(m: nat)
+ ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
+ {
+ m < 75
+ }
- // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
+ // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
+ }
}
module Mojul1 {
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 45d1e598..0eff4874 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -1,25 +1,25 @@ -CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(21,7): Error: unresolved identifier: _k
-CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
-CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause
-CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause
-CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass
+CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared#
+CoResolution.dfy(22,9): Error: unresolved identifier: _k
+CoResolution.dfy(41,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
+CoResolution.dfy(52,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+CoResolution.dfy(70,12): Error: a copredicate is not allowed to declare any reads clause
+CoResolution.dfy(76,33): Error: a copredicate is not allowed to declare any ensures clause
CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(95,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(115,24): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(121,28): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(135,26): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(141,30): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
-CoResolution.dfy(202,13): Error: the type of this expression is underspecified
-CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
+CoResolution.dfy(90,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(99,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(113,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(114,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(119,24): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(125,28): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(133,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(134,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(139,26): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(145,30): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(153,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(155,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(171,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A' could not be determined
+CoResolution.dfy(206,13): Error: the type of this expression is underspecified
+CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined
24 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index d8ff3989..d515e559 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -79,7 +79,7 @@ module A { import X as S default T;
import Y as S default T;
import Z = T;
- static method run() {
+ method run() {
var x := new X.C;
x.m();
var y := new Y.C;
@@ -96,17 +96,17 @@ method NotMain() { abstract module S1 {
import B as S default T;
- static method do()
+ method do()
}
module T1 refines S1 {
- static method do() {
+ method do() {
var x := 3;
}
}
module A1 {
import X as S1 default T1;
- static method run() {
+ method run() {
X.do();
var x := new X.B.C;
x.m();
diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy index 80e5eeae..f7a449b8 100644 --- a/Test/dafny0/CompilationErrors.dfy +++ b/Test/dafny0/CompilationErrors.dfy @@ -5,13 +5,15 @@ type MyType // compile error: opaque type iterator Iter() // compile error: body-less iterator
ghost method M() // compile error: body-less ghost method
method P() // compile error: body-less method
-method Q()
-{
- if g == 0 {
- assume true; // compile error: assume
+class TestClass {
+ method Q()
+ {
+ if g == 0 {
+ assume true; // compile error: assume
+ }
}
+ ghost var g: int;
}
-ghost var g: int;
function F(): int // compile error: body-less ghost function
function method H(): int // compile error: body-less function method
diff --git a/Test/dafny0/CompilationErrors.dfy.expect b/Test/dafny0/CompilationErrors.dfy.expect index e5583f30..f04b5ef8 100644 --- a/Test/dafny0/CompilationErrors.dfy.expect +++ b/Test/dafny0/CompilationErrors.dfy.expect @@ -2,12 +2,12 @@ Dafny program verifier finished with 15 verified, 0 errors
Compilation error: Opaque type ('_module.MyType') cannot be compiled
Compilation error: Iterator _module.Iter has no body
+Compilation error: an assume statement cannot be compiled (line 12)
Compilation error: Method _module._default.M has no body
Compilation error: Method _module._default.P has no body
-Compilation error: an assume statement cannot be compiled (line 11)
Compilation error: Function _module._default.F has no body
Compilation error: Function _module._default.H has no body
-Compilation error: an assume statement cannot be compiled (line 20)
-Compilation error: an assume statement cannot be compiled (line 23)
-Compilation error: an assume statement cannot be compiled (line 28)
-Compilation error: an assume statement cannot be compiled (line 37)
+Compilation error: an assume statement cannot be compiled (line 22)
+Compilation error: an assume statement cannot be compiled (line 25)
+Compilation error: an assume statement cannot be compiled (line 30)
+Compilation error: an assume statement cannot be compiled (line 39)
diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy index 12a4353d..0c539117 100644 --- a/Test/dafny0/ComputationsNeg.dfy +++ b/Test/dafny0/ComputationsNeg.dfy @@ -25,12 +25,12 @@ ghost method test_ThProperty() }
// The following is a test that well-typedness antecednets are included in the literal axioms
-static function StaticFact(n: nat): nat
+function StaticFact(n: nat): nat
ensures 0 < StaticFact(n);
{
if n == 0 then 1 else n * StaticFact(n - 1)
}
-static method test_StaticFact()
+method test_StaticFact()
{
assert StaticFact(0) == 1;
assert 42 != 42; // error: this should fail
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index 1295da96..cfdc2897 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -12,7 +12,7 @@ module CoRecursion { }
function AscendingChainAndRead(n: nat): Stream<int>
- reads this; // with a reads clause, this function is not a co-recusvie function
+ reads null; // with a reads clause, this function is not a co-recusvie function
{
More(n, AscendingChainAndRead(n+1)) // error: cannot prove termination
}
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index b283756b..265fadb5 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -1,33 +1,35 @@ // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
-method M0(S: set<int>) {
- forall s | s in S ensures s < 0;
-}
+class MyClass {
+ method M0(S: set<int>) {
+ forall s | s in S ensures s < 0;
+ }
-method M1(x: int)
-{
- var i := x;
- while (0 < i)
- invariant i <= x;
-}
+ method M1(x: int)
+ {
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+ }
-method M2(x: int)
-{
- var i := x;
- while (0 < i)
- invariant i <= x;
- decreases i;
-}
+ method M2(x: int)
+ {
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+ decreases i;
+ }
-var f: int;
+ var f: int;
-method M3(x: int)
- requires f <= x;
- modifies `f;
-{
- while (0 < f)
- invariant f <= x;
- decreases f;
+ method M3(x: int)
+ requires f <= x;
modifies `f;
+ {
+ while (0 < f)
+ invariant f <= x;
+ decreases f;
+ modifies `f;
+ }
}
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index 366cdfcc..aec38387 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -31,7 +31,7 @@ module Mx { }
}
- static method StaticM(k: nat) returns (m: int)
+ method StaticM(k: nat) returns (m: int)
{
m := k;
}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 14a71178..4814f26f 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -178,11 +178,11 @@ iterator AllocationIterator(x: Cell) }
}
-static method SomeMethod()
+method SomeMethod()
{
}
-static method AnotherMethod() returns (u: Cell, v: Cell)
+method AnotherMethod() returns (u: Cell, v: Cell)
ensures u != null && fresh(u);
{
u := new Cell;
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index dfa09b1e..b9f6a2c5 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -65,49 +65,51 @@ method M4(a: array<int>) returns (r: int) assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];
}
-var index: int;
-method P(a: array<int>) returns (b: bool, ii: int)
- requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
- modifies this, a;
- ensures ii == index;
- // The following uses a variable with a non-old definition inside an old expression:
- ensures 0 <= index < a.Length && old(a[ii]) == 19;
- ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;
- // The following places both the variable and the body inside an old:
- ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);
- // Here, the definition of the variable is old, and it's used both inside and
- // inside an old expression:
- ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;
-{
- b := 0 <= index < a.Length && a[index] == 17;
- var i, j := 0, -1;
- while (i < a.Length)
- invariant 0 <= i <= a.Length;
- invariant forall k :: 0 <= k < i ==> a[k] == 21;
- invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);
- invariant (0 <= j < i && old(a[j]) == 19) ||
- (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);
+class AClass {
+ var index: int;
+ method P(a: array<int>) returns (b: bool, ii: int)
+ requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
+ modifies this, a;
+ ensures ii == index;
+ // The following uses a variable with a non-old definition inside an old expression:
+ ensures 0 <= index < a.Length && old(a[ii]) == 19;
+ ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;
+ // The following places both the variable and the body inside an old:
+ ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);
+ // Here, the definition of the variable is old, and it's used both inside and
+ // inside an old expression:
+ ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;
{
- if (a[i] == 19) { j := i; }
- i, a[i] := i + 1, 21;
+ b := 0 <= index < a.Length && a[index] == 17;
+ var i, j := 0, -1;
+ while (i < a.Length)
+ invariant 0 <= i <= a.Length;
+ invariant forall k :: 0 <= k < i ==> a[k] == 21;
+ invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);
+ invariant (0 <= j < i && old(a[j]) == 19) ||
+ (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);
+ {
+ if (a[i] == 19) { j := i; }
+ i, a[i] := i + 1, 21;
+ }
+ index := j;
+ ii := index;
}
- index := j;
- ii := index;
-}
-method PMain(a: array<int>)
- requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
- modifies this, a;
-{
- var s := a[..];
- var b17, ii := P(a);
- assert s == old(a[..]);
- assert s[index] == 19;
- if (*) {
- assert a[index] == 19; // error (a can have changed in P)
- } else {
- assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;
- assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
+ method PMain(a: array<int>)
+ requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
+ modifies this, a;
+ {
+ var s := a[..];
+ var b17, ii := P(a);
+ assert s == old(a[..]);
+ assert s[index] == 19;
+ if (*) {
+ assert a[index] == 19; // error (a can have changed in P)
+ } else {
+ assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;
+ assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
+ }
}
}
diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index 11a7aebe..b82e06ad 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -1,31 +1,31 @@ -LetExpr.dfy(8,12): Error: assertion violation
+LetExpr.dfy(108,23): Error: assertion violation
Execution trace:
(0,0): anon0
-LetExpr.dfy(107,21): Error: assertion violation
+ (0,0): anon11_Then
+LetExpr.dfy(8,12): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon11_Then
-LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(253,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(256,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(258,24): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes'
+LetExpr.dfy(287,14): Error: RHS is not certain to look like the pattern 'Agnes'
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(304,42): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-LetExpr.dfy(304,12): Error: assertion violation
+LetExpr.dfy(306,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index ac466af2..51e7fe29 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -132,18 +132,20 @@ class Ghosty { ghost method Theorem(a: int) { }
}
-var SomeField: int;
+class AClassWithSomeField {
+ var SomeField: int;
-method SpecialFunctions()
- modifies this;
-{
- SomeField := SomeField + 4;
- var a := old(SomeField); // error: old can only be used in ghost contexts
- var b := fresh(this); // error: fresh can only be used in ghost contexts
- var c := allocated(this); // error: allocated can only be used in ghost contexts
- if (fresh(this)) { // this guard makes the if statement a ghost statement
- ghost var x := old(SomeField); // this is a ghost context, so it's okay
- ghost var y := allocated(this); // this is a ghost context, so it's okay
+ method SpecialFunctions()
+ modifies this;
+ {
+ SomeField := SomeField + 4;
+ var a := old(SomeField); // error: old can only be used in ghost contexts
+ var b := fresh(this); // error: fresh can only be used in ghost contexts
+ var c := allocated(this); // error: allocated can only be used in ghost contexts
+ if (fresh(this)) { // this guard makes the if statement a ghost statement
+ ghost var x := old(SomeField); // this is a ghost context, so it's okay
+ ghost var y := allocated(this); // this is a ghost context, so it's okay
+ }
}
}
@@ -323,3 +325,12 @@ module Q_M { }
class Node { }
}
+
+// ------- top-level statics -----------------
+
+module TopLevelStatics {
+ static function F(): int // error/warning: static keyword does not belong here
+ { 0 }
+ static method M() // error/warning: static keyword does not belong here
+ { }
+}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 90436ed8..0d9d44de 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -1,3 +1,5 @@ +Modules0.dfy(332,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(334,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA
@@ -14,24 +16,24 @@ Modules0.dfy(79,13): Error: expected method call, found expression Modules0.dfy(84,8): Error: type MyClassY does not have a member M
Modules0.dfy(84,9): Error: expected method call, found expression
Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
-Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
-Modules0.dfy(233,13): Error: Undeclared type X in module B
-Modules0.dfy(243,13): Error: unresolved identifier: X
-Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
-Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)
-Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,17): Error: expected method call, found expression
-Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(288,17): Error: expected method call, found expression
-Modules0.dfy(310,24): Error: module Q_Imp does not exist
+Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
+Modules0.dfy(235,13): Error: Undeclared type X in module B
+Modules0.dfy(245,13): Error: unresolved identifier: X
+Modules0.dfy(246,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
+Modules0.dfy(285,12): Error: new can be applied only to reference types (got D)
+Modules0.dfy(288,25): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(289,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(289,17): Error: expected method call, found expression
+Modules0.dfy(290,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(290,17): Error: expected method call, found expression
+Modules0.dfy(312,24): Error: module Q_Imp does not exist
Modules0.dfy(102,6): Error: type MyClassY does not have a member M
Modules0.dfy(102,7): Error: expected method call, found expression
Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(143,11): Error: unresolved identifier: allocated
-Modules0.dfy(146,19): Error: unresolved identifier: allocated
+Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(144,13): Error: unresolved identifier: allocated
+Modules0.dfy(147,21): Error: unresolved identifier: allocated
36 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 2f38e39e..c134bb9a 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -19,7 +19,7 @@ class C { method MyMethod() { }
-var MyField: int;
+
module Babble {
class Z {
@@ -30,7 +30,7 @@ module Babble { }
}
-static function MyFunction(): int { 5 }
+function MyFunction(): int { 5 }
class D { }
diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy index 8b2ff570..6a68c38e 100644 --- a/Test/dafny0/Modules2.dfy +++ b/Test/dafny0/Modules2.dfy @@ -6,14 +6,14 @@ module A { var f: int;
}
datatype D = E(int) | F(int);
- static function f(n:nat): nat
+ function f(n:nat): nat
}
module B {
class C {
var f: int;
}
datatype D = E(int) | F(int);
- static function f(n:nat): nat
+ function f(n:nat): nat
}
module Test {
import opened A; // nice shorthand for import opened A = A; (see below)
@@ -49,7 +49,7 @@ module Test3 { var d := E(i); // bad, as both A and B give a definition of E
var d' := D.E(i); // bad, as D is still itself ambiguous.
var d'':= B.D.E(i); // good, just use the B version
- assert f(3) >= 0; // bad because A and be both define f statically.
+ assert f(3) >= 0; // bad because A and B both define f statically.
}
}
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 78049387..86f8c127 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -10,28 +10,30 @@ method Main() { M(-25); // error: cannot pass -25 as a nat
}
-var f: nat;
+class MyClass {
+ var f: nat;
-method CheckField(x: nat, y: int)
- requires 0 <= y;
- modifies this;
-{
- var y: nat := y;
-
- assert 0 <= f;
- while (0 < y)
+ method CheckField(x: nat, y: int)
+ requires 0 <= y;
+ modifies this;
{
- f := f + 1;
- if (15 < f) {
- f := f - 12;
+ var y: nat := y;
+
+ assert 0 <= f;
+ while (0 < y)
+ {
+ f := f + 1;
+ if (15 < f) {
+ f := f - 12;
+ }
+ y := y - 1;
}
- y := y - 1;
- }
- assert 0 <= f;
+ assert 0 <= f;
- f := x; // no problem
- f := x + 3; // no problem here either
- f := x - 3; // error: cannot prove RHS is a nat
+ f := x; // no problem
+ f := x + 3; // no problem here either
+ f := x - 3; // error: cannot prove RHS is a nat
+ }
}
method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index 7bee017c..99fa16e5 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -1,41 +1,41 @@ -NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon0
-NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(35,12): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
- NatTypes.dfy(22,3): anon10_LoopHead
+ NatTypes.dfy(23,5): anon10_LoopHead
(0,0): anon10_LoopBody
- NatTypes.dfy(22,3): anon11_Else
+ NatTypes.dfy(23,5): anon11_Else
(0,0): anon12_Then
-NatTypes.dfy(41,14): Error: assertion violation
+NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
- (0,0): anon4_Then
NatTypes.dfy(43,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-NatTypes.dfy(60,16): Error: assertion violation
+NatTypes.dfy(45,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+NatTypes.dfy(62,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(74,16): Error: assertion violation
+NatTypes.dfy(76,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(92,22): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(94,22): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-NatTypes.dfy(130,35): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/Newtypes.dfy b/Test/dafny0/Newtypes.dfy index db737f68..93caa7ab 100644 --- a/Test/dafny0/Newtypes.dfy +++ b/Test/dafny0/Newtypes.dfy @@ -53,7 +53,7 @@ module Constraints { newtype B = x: A | x < 100
newtype C = B // the constraints 0 <= x < 100 still apply
- static predicate IsEven(x: int) // note that this is a ghost predicate
+ predicate IsEven(x: int) // note that this is a ghost predicate
{
x % 2 == 0
}
diff --git a/Test/dafny0/NewtypesResolution.dfy b/Test/dafny0/NewtypesResolution.dfy index dbf9a175..9ae657b7 100644 --- a/Test/dafny0/NewtypesResolution.dfy +++ b/Test/dafny0/NewtypesResolution.dfy @@ -80,7 +80,7 @@ module Constraints { newtype B = x: A | x < 100
newtype C = B // the constraints 0 <= x < 100 still apply
- static predicate IsEven(x: int) // note that this is a ghost predicate
+ predicate IsEven(x: int) // note that this is a ghost predicate
{
x % 2 == 0
}
@@ -103,7 +103,7 @@ module WrongNumberOfArguments { module CyclicDependencies {
newtype Cycle = x: int | (BadLemma(); false) // error: cycle
- static lemma BadLemma()
+ lemma BadLemma()
ensures false;
{
var c: Cycle;
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index d343a84d..030eb350 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -209,7 +209,7 @@ class TwoState_C { ghost var data: int; } // It is not possible to achieve this postcondition in a ghost method, because ghost
// contexts are not allowed to allocate state. Callers of this ghost method will know
// that the postcondition is tantamount to 'false'.
-ghost static method TwoState0(y: int)
+ghost method TwoState0(y: int)
ensures exists o: TwoState_C :: o != null && fresh(o);
method TwoState_Main0() {
@@ -261,39 +261,41 @@ method TwoState_Main3() // ------- empty forall statement -----------------------------------------
-var emptyPar: int;
+class EmptyForallStatement {
+ var emptyPar: int;
-method Empty_Parallel0()
- modifies this;
- ensures emptyPar == 8;
-{
- forall () {
- this.emptyPar := 8;
+ method Empty_Parallel0()
+ modifies this;
+ ensures emptyPar == 8;
+ {
+ forall () {
+ this.emptyPar := 8;
+ }
}
-}
-function EmptyPar_P(x: int): bool
-ghost method EmptyPar_Lemma(x: int)
- ensures EmptyPar_P(x);
+ function EmptyPar_P(x: int): bool
+ ghost method EmptyPar_Lemma(x: int)
+ ensures EmptyPar_P(x);
-method Empty_Parallel1()
- ensures EmptyPar_P(8);
-{
- forall {
- EmptyPar_Lemma(8);
+ method Empty_Parallel1()
+ ensures EmptyPar_P(8);
+ {
+ forall {
+ EmptyPar_Lemma(8);
+ }
}
-}
-method Empty_Parallel2()
-{
- forall
- ensures exists k :: EmptyPar_P(k);
+ method Empty_Parallel2()
{
- var y := 8;
- assume EmptyPar_P(y);
+ forall
+ ensures exists k :: EmptyPar_P(k);
+ {
+ var y := 8;
+ assume EmptyPar_P(y);
+ }
+ assert exists k :: EmptyPar_P(k); // yes
+ assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this
}
- assert exists k :: EmptyPar_P(k); // yes
- assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this
}
// ---------------------------------------------------------------------
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect index 6b726cd5..db551bba 100644 --- a/Test/dafny0/Parallel.dfy.expect +++ b/Test/dafny0/Parallel.dfy.expect @@ -1,3 +1,7 @@ +Parallel.dfy(297,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
Execution trace:
@@ -60,9 +64,5 @@ Execution trace: (0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon5
-Parallel.dfy(296,20): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
Dafny program verifier finished with 43 verified, 9 errors
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index 1a9a3257..a92e647a 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -38,30 +38,36 @@ module B refines A { // ------------------------------------------------ module A_AnonymousClass { - var x: int; - method Increment(d: int) - modifies this; - { - x := x + d; + class XX { + var x: int; + method Increment(d: int) + modifies this; + { + x := x + d; + } } } module B_AnonymousClass refines A_AnonymousClass { - method Increment... - ensures x <= old(x) + d; + class XX { + method Increment... + ensures x <= old(x) + d; + } } module C_AnonymousClass refines B_AnonymousClass { - method Increment(d: int) - ensures old(x) + d <= x; - method Main() - modifies this; - { - x := 25; - Increment(30); - assert x == 55; - Increment(12); - assert x == 66; // error: it's 67 + class XX { + method Increment(d: int) + ensures old(x) + d <= x; + method Main() + modifies this; + { + x := 25; + Increment(30); + assert x == 55; + Increment(12); + assert x == 66; // error: it's 67 + } } } diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect index d214565b..93d59873 100644 --- a/Test/dafny0/Refinement.dfy.expect +++ b/Test/dafny0/Refinement.dfy.expect @@ -6,35 +6,35 @@ Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this re Refinement.dfy(33,20): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(64,14): Error: assertion violation
+Refinement.dfy(69,16): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(74,17): Error: assertion violation
+Refinement.dfy(80,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(72,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(99,12): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(78,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(77,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(102,3): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(83,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(180,9): Related location
+Refinement.dfy(189,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](121,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,9): Related location
Execution trace:
(0,0): anon0
-Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(180,9): Related location
+Refinement.dfy(193,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](129,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,9): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Refinement.dfy(193,7): Error: assertion violation
-Refinement.dfy[IncorrectConcrete](131,24): Related location
+Refinement.dfy(199,7): Error: assertion violation
+Refinement.dfy[IncorrectConcrete](137,24): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy index 70d0b989..052918d0 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy +++ b/Test/dafny0/RefinementModificationChecking.dfy @@ -2,25 +2,29 @@ // RUN: %diff "%s.expect" "%t"
abstract module R1 {
- var f: int;
- method m(y: set<int>) returns (r: int)
- modifies this;
- {
- var t := y;
+ class HappyBay {
+ var f: int;
+ method m(y: set<int>) returns (r: int)
+ modifies this;
+ {
+ var t := y;
+ }
}
}
module R2 refines R1 {
- var g: nat;
- method m ...
- {
- ...;
- var x := 3;
- t := {1}; // error: previous local
- r := 3; // error: out parameter
- f := 4; // error: previously defined field
- x := 6; // fine: new local
- g := 34;// fine: new field
+ class HappyBay {
+ var g: nat;
+ method m ...
+ {
+ ...;
+ var x := 3;
+ t := {1}; // error: previous local
+ r := 3; // error: out parameter
+ f := 4; // error: previously defined field
+ x := 6; // fine: new local
+ g := 34;// fine: new field
+ }
}
}
diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect index 675d244e..1a5df922 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy.expect +++ b/Test/dafny0/RefinementModificationChecking.dfy.expect @@ -1,6 +1,6 @@ -RefinementModificationChecking.dfy(19,4): Error: refinement method cannot assign to variable defined in parent module ('t')
-RefinementModificationChecking.dfy(20,4): Error: refinement method cannot assign to variable defined in parent module ('r')
-RefinementModificationChecking.dfy(21,4): Error: refinement method cannot assign to a field defined in parent module ('f')
-RefinementModificationChecking.dfy(47,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
-RefinementModificationChecking.dfy(49,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
+RefinementModificationChecking.dfy(22,6): Error: refinement method cannot assign to variable defined in parent module ('t')
+RefinementModificationChecking.dfy(23,6): Error: refinement method cannot assign to variable defined in parent module ('r')
+RefinementModificationChecking.dfy(24,6): Error: refinement method cannot assign to a field defined in parent module ('f')
+RefinementModificationChecking.dfy(51,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
+RefinementModificationChecking.dfy(53,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
5 resolution/type errors detected in RefinementModificationChecking.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 2f340557..4b290bb7 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -78,25 +78,27 @@ datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int); datatype Rst = David(x: int, y: int);
function Tuv(arg0: Abc, arg1: bool): int { 10 }
-var Eleanor: bool;
-
-method TestNameResolution1() {
- var a0 := Abel;
- var a1 := Alberta;
- var b0 := Benny; // error: there's more than one constructor with the name Benny; needs qualification
- var b1 := Abc.Benny;
- var b2 := Xyz.Benny;
- var Benny := 15; // introduce a local variable with the name 'Benny'
- var b3 := Benny;
- var d0 := David(20); // error: constructor name David is ambiguous
- var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does
- // not match either of them)
- var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given
- // parameters match the signature of only one of those constructors)
- var d3 := Abc.David(20, 40); // error: wrong number of parameters
- var d4 := Rst.David(20, 40);
- var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
- assert Tuv(Abc.Eleanor, e) == 10;
+
+class EE {
+ var Eleanor: bool;
+ method TestNameResolution1() {
+ var a0 := Abel;
+ var a1 := Alberta;
+ var b0 := Benny; // error: there's more than one constructor with the name Benny; needs qualification
+ var b1 := Abc.Benny;
+ var b2 := Xyz.Benny;
+ var Benny := 15; // introduce a local variable with the name 'Benny'
+ var b3 := Benny;
+ var d0 := David(20); // error: constructor name David is ambiguous
+ var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does
+ // not match either of them)
+ var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given
+ // parameters match the signature of only one of those constructors)
+ var d3 := Abc.David(20, 40); // error: wrong number of parameters
+ var d4 := Rst.David(20, 40);
+ var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
+ assert Tuv(Abc.Eleanor, e) == 10;
+ }
}
// --------------- ghost tests -------------------------------------
@@ -386,34 +388,35 @@ method TestCalc(m: int, n: int, a: bool, b: bool) }
}
-/* Side-effect checks */
-ghost var ycalc: int;
+class SideEffectChecks {
+ ghost var ycalc: int;
-ghost method Mod(a: int)
- modifies this;
- ensures ycalc == a;
-{
- ycalc := a;
-}
+ ghost method Mod(a: int)
+ modifies this;
+ ensures ycalc == a;
+ {
+ ycalc := a;
+ }
-ghost method Bad()
- modifies this;
- ensures 0 == 1;
-{
- var x: int;
- calc {
- 0;
- { Mod(0); } // methods with side-effects are not allowed
- ycalc;
- { ycalc := 1; } // heap updates are not allowed
- 1;
- { x := 1; } // updates to locals defined outside of the hint are not allowed
- x;
- {
- var x: int;
- x := 1; // this is OK
+ ghost method Bad()
+ modifies this;
+ ensures 0 == 1;
+ {
+ var x: int;
+ calc {
+ 0;
+ { Mod(0); } // methods with side-effects are not allowed
+ ycalc;
+ { ycalc := 1; } // heap updates are not allowed
+ 1;
+ { x := 1; } // updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
}
- 1;
}
}
@@ -648,9 +651,9 @@ module UnderspecifiedTypes { // ------------------------- lemmas ------------------------------
// a lemma is allowed to have out-parameters, but not a modifies clause
-lemma MyLemma(x: int) returns (y: int)
+lemma MyLemma(x: int, l: Lamb) returns (y: int)
requires 0 <= x;
- modifies this;
+ modifies l;
ensures 0 <= y;
{
y := x;
@@ -659,110 +662,112 @@ lemma MyLemma(x: int) returns (y: int) // ------------------------- statements in expressions ------------------------------
module StatementsInExpressions {
- ghost method SideEffect()
- modifies this;
- {
- }
-
- method NonGhostMethod()
- {
- }
+ class MyClass {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
- ghost method M()
- modifies this;
- {
- calc {
- 5;
- { SideEffect(); } // error: cannot call method with side effects
- 5;
+ method NonGhostMethod()
+ {
}
- }
- function F(): int
- {
- calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects
+ 5;
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
+ }
+
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
- 6;
+ 5
}
- 5
- }
- var MyField: int;
- ghost var MyGhostField: int;
+ var MyField: int;
+ ghost var MyGhostField: int;
- method N()
- {
- var y :=
- calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { M(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
- 6;
+ 5;
}
- 5;
- }
- ghost method MyLemma()
- ghost method MyGhostMethod()
- modifies this;
- method OrdinaryMethod()
- ghost method OutParamMethod() returns (y: int)
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
- function UseLemma(): int
- {
- MyLemma();
- MyGhostMethod(); // error: modifies state
- OrdinaryMethod(); // error: not a ghost
- OutParamMethod(); // error: has out-parameters
- 10
+ function UseLemma(): int
+ {
+ MyLemma();
+ MyGhostMethod(); // error: modifi2es state
+ OrdinaryMethod(); // error: not a ghost
+ OutParamMethod(); // error: has out-parameters
+ 10
+ }
}
}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 9ba6a1b3..55a4b1e6 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,125 +1,133 @@ -ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
-ResolutionErrors.dfy(558,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(565,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements
-ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context
-ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(619,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(686,22): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(702,18): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(724,22): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(734,9): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(762,17): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(764,18): Error: wrong number of method result arguments (got 0, expected 1)
-ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object)
-ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object)
-ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
-ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
-ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
-ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
-ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1000,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
-ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1019,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
+ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(611,10): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(704,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(736,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
+ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
+ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
+ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
+ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
-ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
-ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
-ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
-ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)
-ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)
-ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1286,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
-ResolutionErrors.dfy(1296,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor
+ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
+ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
-ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(117,10): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(149,10): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor
-ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x
-ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(1041,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
+ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
+ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(446,9): Error: class Lamb does not have a anonymous constructor
+ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
@@ -133,53 +141,45 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
-ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
-ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(96,16): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(263,2): Error: duplicate label
-ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,9): Error: a constructor is allowed to be called only when an object is being allocated
-ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(345,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
-ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(406,9): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint
-ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
-ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
-ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
-ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(931,16): Error: condition is expected to be of type bool, but is int
-ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
-ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
-ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
-ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
-ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1129,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
-ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(265,2): Error: duplicate label
+ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(386,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(544,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(546,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(548,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
184 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7d8628a9..13f56383 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -511,7 +511,7 @@ class AttributeTests { // ----------------------- test attributes on variable declarations --------
-static method TestAttributesVarDecls()
+method TestAttributesVarDecls()
{
var {:foo foo} foo := null;
var {:bar bar} bar := 0;
@@ -521,7 +521,7 @@ static method TestAttributesVarDecls() // ----------------------- Pretty printing of !(!expr) --------
-static method TestNotNot()
+method TestNotNot()
{
assert !(!true); // Shouldn't pretty print as "!!true".
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 70c30aa6..0e51ade2 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -201,50 +201,51 @@ method DecreasesYieldsAnInvariant(z: int) { // ----------------------- top elements --------------------------------------
-var count: int;
+class TopElements {
+ var count: int;
-// Here is the old way that this had to be specified:
+ // Here is the old way that this had to be specified:
-method OuterOld(a: int)
- modifies this;
- decreases a, true;
-{
- count := count + 1;
- InnerOld(a, count);
-}
+ method OuterOld(a: int)
+ modifies this;
+ decreases a, true;
+ {
+ count := count + 1;
+ InnerOld(a, count);
+ }
-method InnerOld(a: int, b: int)
- modifies this;
- decreases a, false, b;
-{
- count := count + 1;
- if (b == 0 && 1 <= a) {
- OuterOld(a - 1);
- } else if (1 <= b) {
- InnerOld(a, b - 1);
+ method InnerOld(a: int, b: int)
+ modifies this;
+ decreases a, false, b;
+ {
+ count := count + 1;
+ if (b == 0 && 1 <= a) {
+ OuterOld(a - 1);
+ } else if (1 <= b) {
+ InnerOld(a, b - 1);
+ }
}
-}
-// Now the default specifications ("decreases a;" and "decreases a, b;") suffice:
+ // Now the default specifications ("decreases a;" and "decreases a, b;") suffice:
-method Outer(a: int)
- modifies this;
-{
- count := count + 1;
- Inner(a, count);
-}
+ method Outer(a: int)
+ modifies this;
+ {
+ count := count + 1;
+ Inner(a, count);
+ }
-method Inner(a: int, b: int)
- modifies this;
-{
- count := count + 1;
- if (b == 0 && 1 <= a) {
- Outer(a - 1);
- } else if (1 <= b) {
- Inner(a, b - 1);
+ method Inner(a: int, b: int)
+ modifies this;
+ {
+ count := count + 1;
+ if (b == 0 && 1 <= a) {
+ Outer(a - 1);
+ } else if (1 <= b) {
+ Inner(a, b - 1);
+ }
}
}
-
// -------------------------- decrease either datatype value -----------------
function Zipper0<T>(a: List<T>, b: List<T>): List<T>
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index fd86c8cb..98aa0cd8 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -1,7 +1,7 @@ -Termination.dfy[TerminationRefinement1](440,6): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](441,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Termination.dfy(360,47): Error: failure to decrease termination measure
+Termination.dfy(361,47): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon7_Else
@@ -41,18 +41,18 @@ Execution trace: (0,0): anon10_Then
(0,0): anon5
Termination.dfy(125,3): anon11_Else
-Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(295,3): Error: decreases expression might not decrease
+Termination.dfy(296,3): Error: decreases expression might not decrease
Execution trace:
- Termination.dfy(295,3): anon9_LoopHead
+ Termination.dfy(296,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(295,3): anon10_Else
- Termination.dfy(295,3): anon11_Else
+ Termination.dfy(296,3): anon10_Else
+ Termination.dfy(296,3): anon11_Else
(0,0): anon12_Else
Dafny program verifier finished with 62 verified, 8 errors
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index d5c6a9d2..1e4f928a 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -28,7 +28,7 @@ method BadLemma(c0: Color, c1: Color) var w1 := Wrapper.Wrap(c1);
// Manually, add the following assertions in Boogie. (These would
- // be ill-typed in Dafny.)
+ // b93e ill-typed in Dafny.)
// assert _default.F($Heap, this, w#06);
// assert _default.F($Heap, this, w#17);
@@ -68,7 +68,8 @@ method M(list: List, S: set<MyClass>) returns (ret: int) }
var k := N();
assert k.H() == 5;
- ghost var l := NF();
+ var st := new State;
+ ghost var l := st.NF();
assert l != null ==> l.H() == 5;
forall s | s in S ensures true; { assert s == null || s.H() == 5; }
@@ -90,8 +91,11 @@ method N() returns (k: MyClass) {
k := new MyClass;
}
-var a: MyClass;
-function NF(): MyClass reads this; { a }
+
+class State {
+ var a: MyClass;
+ function NF(): MyClass reads this; { a }
+}
function TakesADatatype(a: List): int { 12 }
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index aa3d7671..f066d13f 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -105,7 +105,7 @@ class CClient { // -------------------------
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+function IsCelebrity<Person>(c: Person, people: set<Person>): bool
requires c == c || c in people;
{
false
@@ -119,7 +119,7 @@ method FindCelebrity3(people: set<int>, ghost c: int) b := F(c, people);
}
-static function F(c: int, people: set<int>): bool
+function F(c: int, people: set<int>): bool
requires IsCelebrity(c, people);
{
false
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index 3a0828d4..75277b8b 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -7,11 +7,11 @@ Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); Dafny program verifier finished with 3 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
- >>> added axiom: (forall call1old#AT#$Heap: Heap :: { ##extracted_function##1(call1old#AT#$Heap) } ##extracted_function##1(call1old#AT#$Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap)))
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call1old#AT#$Heap);
+ >>> added axiom: (forall call0old#AT#$Heap: Heap :: { ##extracted_function##1(call0old#AT#$Heap) } ##extracted_function##1(call0old#AT#$Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);
Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call1old#AT#$Heap);
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
>>> MarkAsPartiallyVerified
@@ -49,13 +49,13 @@ Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f >>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,11)) assert this == this;
+Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this));
+Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,11)) assert this == this;
+Processing command (at Snapshots2.v0.dfy(14,11)) assert true;
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this));
+Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
>>> DoNothingToAssert
@@ -72,13 +72,13 @@ Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); Snapshots2.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
-Processing command (at Snapshots2.v1.dfy(11,11)) assert this == this;
+Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this));
+Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));
>>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,11)) assert this == this;
+Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this));
+Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 360c5aba..fb7a5fab 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -3,10 +3,10 @@ // Celebrity example, inspired by the Rodin tutorial
-static function method Knows<X>(a: X, b: X): bool
+function method Knows<X>(a: X, b: X): bool
requires a != b; // forbid asking about the reflexive case
-static function IsCelebrity<Y>(c: Y, people: set<Y>): bool
+function IsCelebrity<Y>(c: Y, people: set<Y>): bool
{
c in people &&
(forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 10b70e09..174e71c8 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -8,7 +8,7 @@ datatype Expr = Var(int) |
Nary(int, List);
-static function Subst(e: Expr, v: int, val: int): Expr
+function Subst(e: Expr, v: int, val: int): Expr
{
match e
case Const(c) => e
@@ -16,14 +16,14 @@ static function Subst(e: Expr, v: int, val: int): Expr case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
}
-static function SubstList(l: List, v: int, val: int): List
+function SubstList(l: List, v: int, val: int): List
{
match l
case Nil => l
case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
}
-static ghost method Theorem(e: Expr, v: int, val: int)
+lemma Theorem(e: Expr, v: int, val: int)
ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
{
match e {
@@ -34,7 +34,7 @@ static ghost method Theorem(e: Expr, v: int, val: int) }
}
-static ghost method Lemma(l: List, v: int, val: int)
+lemma Lemma(l: List, v: int, val: int)
ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
{
match l {
@@ -52,7 +52,7 @@ datatype Expression = Var(int) |
Nary(int, seq<Expression>);
-static function Substitute(e: Expression, v: int, val: int): Expression
+function Substitute(e: Expression, v: int, val: int): Expression
decreases e;
{
match e
@@ -61,7 +61,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
}
-static function SubstSeq(/*ghost*/ parent: Expression,
+function SubstSeq(/*ghost*/ parent: Expression,
q: seq<Expression>, v: int, val: int): seq<Expression>
requires (forall a :: a in q ==> a < parent);
decreases parent, q;
@@ -70,7 +70,7 @@ static function SubstSeq(/*ghost*/ parent: Expression, SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
}
-static ghost method TheoremSeq(e: Expression, v: int, val: int)
+lemma TheoremSeq(e: Expression, v: int, val: int)
ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
{
match e {
@@ -97,7 +97,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) }
}
-static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
+lemma LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index 763cef1b..beb1597e 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -7,13 +7,13 @@ datatype List<T> = Nil | Cons(T, List<T>); datatype Tree = Node(int, List<Tree>);
-static function Inc(t: Tree): Tree
+function Inc(t: Tree): Tree
{
match t
case Node(n, children) => Tree.Node(n+1, ForestInc(children))
}
-static function ForestInc(forest: List<Tree>): List<Tree>
+function ForestInc(forest: List<Tree>): List<Tree>
{
match forest
case Nil => forest
@@ -24,13 +24,13 @@ static function ForestInc(forest: List<Tree>): List<Tree> datatype GTree<T> = Node(T, List<GTree<T>>);
-static function GInc(t: GTree<int>): GTree<int>
+function GInc(t: GTree<int>): GTree<int>
{
match t
case Node(n, children) => GTree.Node(n+1, GForestInc(children))
}
-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
+function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
{
match forest
case Nil => forest
@@ -43,13 +43,13 @@ datatype TreeList = Nil | Cons(OneTree, TreeList); datatype OneTree = Node(int, TreeList);
-static function XInc(t: OneTree): OneTree
+function XInc(t: OneTree): OneTree
{
match t
case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
}
-static function XForestInc(forest: TreeList): TreeList
+function XForestInc(forest: TreeList): TreeList
{
match forest
case Nil => forest
diff --git a/Test/dafny2/Intervals.dfy b/Test/dafny2/Intervals.dfy index df14c1e9..ef40910e 100644 --- a/Test/dafny2/Intervals.dfy +++ b/Test/dafny2/Intervals.dfy @@ -4,63 +4,65 @@ // The RoundDown and RoundUp methods in this file are the ones in the Boogie
// implementation Source/AbsInt/IntervalDomain.cs.
-var thresholds: array<int>;
+class Rounding {
+ var thresholds: array<int>;
-function Valid(): bool
- reads this, thresholds;
-{
- thresholds != null &&
- forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
-}
-
-method RoundDown(k: int) returns (r: int)
- requires Valid();
- ensures -1 <= r < thresholds.Length;
- ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
- ensures 0 <= r ==> thresholds[r] <= k;
-{
- if (thresholds.Length == 0 || k < thresholds[0]) {
- return -1;
+ function Valid(): bool
+ reads this, thresholds;
+ {
+ thresholds != null &&
+ forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
}
- var i, j := 0, thresholds.Length - 1;
- while (i < j)
- invariant 0 <= i <= j < thresholds.Length;
- invariant thresholds[i] <= k;
- invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
+
+ method RoundDown(k: int) returns (r: int)
+ requires Valid();
+ ensures -1 <= r < thresholds.Length;
+ ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
+ ensures 0 <= r ==> thresholds[r] <= k;
{
- var mid := i + (j - i + 1) / 2;
- assert i < mid <= j;
- if (thresholds[mid] <= k) {
- i := mid;
- } else {
- j := mid - 1;
+ if (thresholds.Length == 0 || k < thresholds[0]) {
+ return -1;
}
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant thresholds[i] <= k;
+ invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
+ {
+ var mid := i + (j - i + 1) / 2;
+ assert i < mid <= j;
+ if (thresholds[mid] <= k) {
+ i := mid;
+ } else {
+ j := mid - 1;
+ }
+ }
+ return i;
}
- return i;
-}
-method RoundUp(k: int) returns (r: int)
- requires Valid();
- ensures 0 <= r <= thresholds.Length;
- ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
- ensures r < thresholds.Length ==> k <= thresholds[r];
-{
- if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
- return thresholds.Length;
- }
- var i, j := 0, thresholds.Length - 1;
- while (i < j)
- invariant 0 <= i <= j < thresholds.Length;
- invariant k <= thresholds[j];
- invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
+ method RoundUp(k: int) returns (r: int)
+ requires Valid();
+ ensures 0 <= r <= thresholds.Length;
+ ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
+ ensures r < thresholds.Length ==> k <= thresholds[r];
{
- var mid := i + (j - i) / 2;
- assert i <= mid < j;
- if (thresholds[mid] < k) {
- i := mid + 1;
- } else {
- j := mid;
+ if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
+ return thresholds.Length;
+ }
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant k <= thresholds[j];
+ invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
+ {
+ var mid := i + (j - i) / 2;
+ assert i <= mid < j;
+ if (thresholds[mid] < k) {
+ i := mid + 1;
+ } else {
+ j := mid;
+ }
}
+ return i;
}
- return i;
}
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 2244f37f..7ea038be 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -3,23 +3,23 @@ abstract module TotalOrder {
type T // the type to be compared
- static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
+ predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
// Three properties of total orders. Here, they are given as unproved
// lemmas, that is, as axioms.
- static lemma Antisymmetry(a: T, b: T)
+ lemma Antisymmetry(a: T, b: T)
requires Leq(a, b) && Leq(b, a);
ensures a == b;
- static lemma Transitivity(a: T, b: T, c: T)
+ lemma Transitivity(a: T, b: T, c: T)
requires Leq(a, b) && Leq(b, c);
ensures Leq(a, c);
- static lemma Totality(a: T, b: T)
+ lemma Totality(a: T, b: T)
ensures Leq(a, b) || Leq(b, a);
}
abstract module Sort {
import O as TotalOrder // let O denote some module that has the members of TotalOrder
- static predicate Sorted(a: array<O.T>, low: int, high: int)
+ predicate Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
// The body of the predicate is hidden outside the module, but the postcondition is
@@ -32,7 +32,7 @@ abstract module Sort { // In the insertion sort routine below, it's more convenient to keep track of only that
// neighboring elements of the array are sorted...
- static predicate NeighborSorted(a: array<O.T>, low: int, high: int)
+ predicate NeighborSorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
{
@@ -40,7 +40,7 @@ abstract module Sort { }
// ...but we show that property to imply all pairs to be sorted. The proof of this
// lemma uses the transitivity property.
- static lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)
+ lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
requires NeighborSorted(a, low, high);
ensures Sorted(a, low, high);
@@ -56,7 +56,7 @@ abstract module Sort { }
// Standard insertion sort method
- static method InsertionSort(a: array<O.T>)
+ method InsertionSort(a: array<O.T>)
requires a != null;
modifies a;
ensures Sorted(a, 0, a.Length);
@@ -96,30 +96,30 @@ module IntOrder refines TotalOrder { // (If there were type synonyms, we could perhaps have written just "type T = int".)
datatype T = Int(i: int)
// Define the ordering on these integers
- static predicate method Leq ...
+ predicate method Leq ...
ensures Leq(a, b) ==> a.i <= b.i;
{
a.i <= b.i
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
// Another example of a TotalOrder. Now we can sort pairs of integers.
// Lexiographic ordering of pairs of integers
module IntLexOrder refines TotalOrder {
datatype T = Int(i: int, j: int)
- static predicate method Leq ... {
+ predicate method Leq ... {
if a.i < b.i then true
else if a.i == b.i then a.j <= b.j
else false
}
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
@@ -129,7 +129,7 @@ module Client { import O = IntOrder
}
import I = IntOrder
- static method TheMain() {
+ method TheMain() {
var a := new I.T[4];
a[0] := I.T.Int(6); // alternatively, we could have written the RHS as: IntSort.O.T.Int(6)
a[1] := I.T.Int(1);
@@ -155,16 +155,16 @@ module intOrder refines TotalOrder { // Instantiate type T with a datatype wrapper around an integer.
type T = int
// Define the ordering on these integers
- static predicate method Leq ...
+ predicate method Leq ...
ensures Leq(a, b) ==> a <= b;
{
a <= b
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
module AnotherClient {
@@ -172,7 +172,7 @@ module AnotherClient { import O = intOrder
}
import I = intOrder
- static method TheMain() {
+ method TheMain() {
var a := new int[4]; // alternatively, could have written 'new I.T[4]'
a[0] := 6;
a[1] := 1;
diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy index 9e7c5460..a221f818 100644 --- a/Test/hofs/Monads.dfy +++ b/Test/hofs/Monads.dfy @@ -4,22 +4,22 @@ abstract module Monad { type M<A>; - static function method Return(x: A): M<A> - static function method Bind(m: M<A>, f:A -> M<B>):M<B> + function method Return(x: A): M<A> + function method Bind(m: M<A>, f:A -> M<B>):M<B> reads f.reads; requires forall a :: f.requires(a); // return x >>= f = f x - static lemma LeftIdentity(x : A, f : A -> M<B>) + lemma LeftIdentity(x : A, f : A -> M<B>) requires forall a :: f.requires(a); ensures Bind(Return(x),f) == f(x); // m >>= return = m - static lemma RightIdentity(m : M<A>) + lemma RightIdentity(m : M<A>) ensures Bind(m,Return) == m; // (m >>= f) >>= g = m >>= (x => f(x) >>= g) - static lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>) requires forall a :: f.requires(a); requires forall b :: g.requires(b); ensures Bind(Bind(m,f),g) == @@ -32,24 +32,24 @@ abstract module Monad { module Identity refines Monad { datatype M<A> = I(A); - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { I(x) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { var I(x) := m; f(x) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { assert Bind(m,Return) == m; } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { assert Bind(Bind(m,f),g) == @@ -64,26 +64,26 @@ module Identity refines Monad { module Maybe refines Monad { datatype M<A> = Just(A) | Nothing; - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { Just(x) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { match m case Nothing => Nothing case Just(x) => f(x) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { assert Bind(m,Return) == m; } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { assert Bind(Bind(m,f),g) == @@ -98,24 +98,24 @@ module Maybe refines Monad { module List refines Monad { datatype M<A> = Cons(hd: A,tl: M<A>) | Nil; - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { Cons(x,Nil) } - static function method Concat(xs: M<A>, ys: M<A>): M<A> + function method Concat(xs: M<A>, ys: M<A>): M<A> { match xs case Nil => ys case Cons(x,xs) => Cons(x,Concat(xs,ys)) } - static function method Join(xss: M<M<A>>) : M<A> + function method Join(xss: M<M<A>>) : M<A> { match xss case Nil => Nil case Cons(xs,xss) => Concat(xs,Join(xss)) } - static function method Map(xs: M<A>, f: A -> B):M<B> + function method Map(xs: M<A>, f: A -> B):M<B> reads f.reads; requires forall a :: f.requires(a); { @@ -124,12 +124,12 @@ module List refines Monad { case Cons(x,xs) => Cons(f(x),Map(xs,f)) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { Join(Map(m,f)) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { calc { Bind(Return(x),f); @@ -141,7 +141,7 @@ module List refines Monad { } } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { match m case Nil => calc { @@ -166,11 +166,11 @@ module List refines Monad { } } - static lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>) + lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>) ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs)); {} - static lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>) + lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>) requires forall a :: f.requires(a); ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f)); { @@ -194,7 +194,7 @@ module List refines Monad { } } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { match m case Nil => calc { diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 1e54f02f..e9280a9a 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -104,7 +104,7 @@ class SparseArray<T> { }
/* The following method is here only to simulate support of arrays in Dafny */
-/*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+/*private*/ method AllocateArray<G>(n: int) returns (arr: seq<G>)
requires 0 <= n;
ensures |arr| == n;
{
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index 2d724b54..b111a438 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -231,21 +231,21 @@ class BreadthFirstSearch<Vertex(==)> }
}
-static function domain<T, U>(m: map<T, U>): set<T>
+function domain<T, U>(m: map<T, U>): set<T>
{
set t | t in m
}
datatype List<T> = Nil | Cons(head: T, tail: List)
-static function length(list: List): nat
+function length(list: List): nat
{
match list
case Nil => 0
case Cons(_, tail) => 1 + length(tail)
}
-static function elements<T>(list: List<T>): set<T>
+function elements<T>(list: List<T>): set<T>
{
match list
case Nil => {}
|