diff options
Diffstat (limited to 'Test/VSComp2010')
| -rw-r--r-- | Test/VSComp2010/Problem2-Invert.dfy | 2 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem3-FindZero.dfy | 2 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem4-Queens.dfy | 2 |
3 files changed, 3 insertions, 3 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 ==>
|