diff options
| author |  Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
| commit | 7ee036cae0cc6a2d48786f18908f26de37136236 (patch) | |
| tree | d8e3965854d7499f754551695f694cee8a7acbe5 /Test/VSComp2010 | |
| parent | 5152d9cd2fd4cd7258d745ec01324b4b654e1172 (diff) | |
Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
Diffstat (limited to 'Test/VSComp2010')
| -rw-r--r-- | Test/VSComp2010/Problem4-Queens.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 2f21b7a1..2d4111db 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -34,7 +34,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) |board| == N &&
(forall p :: 0 <= p && p < N ==> IsConsistent(board, p));
ensures !success ==>
- (forall B ::
+ (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N)
==>
(exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
@@ -66,7 +66,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: |newBoard| == N &&
(forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p));
ensures !success ==>
- (forall B ::
+ (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
boardSoFar <= B
==>
@@ -84,7 +84,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: var n := 0;
while (n < N)
invariant n <= N;
- invariant (forall B ::
+ invariant (forall B: seq<int> ::
// For any board 'B' with 'N' queens, each placed in an existing row
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
// ... where 'B' is an extension of 'boardSoFar'
@@ -122,7 +122,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: } else {
// Since 'n' is not a consistent placement for a queen in column 'pos', there is also
// no extension of 'candidateBoard' that would make the entire board consistent.
- assert (forall B ::
+ assert (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
candidateBoard <= B
==>
|