diff options
Diffstat (limited to 'Test/VSComp2010')
| -rw-r--r-- | Test/VSComp2010/Problem1-SumMax.dfy | 4 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem2-Invert.dfy | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy index be7cc2c8..1b105ac1 100644 --- a/Test/VSComp2010/Problem1-SumMax.dfy +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -8,7 +8,7 @@ // the requested postcondition.
method M(N: int, a: array<int>) returns (sum: int, max: int)
- requires 0 <= N && a != null && |a| == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]);
+ requires 0 <= N && a != null && a.Length == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]);
ensures sum <= N * max;
{
sum := 0;
@@ -39,5 +39,5 @@ method Main() a[8] := 10;
a[9] := 6;
call s, m := M(10, a);
- print "N = ", |a|, " sum = ", s, " max = ", m, "\n";
+ print "N = ", a.Length, " sum = ", s, " max = ", m, "\n";
}
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 63da4cb5..bf6aca37 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -23,7 +23,7 @@ // connect the two.
method M(N: int, A: array<int>, B: array<int>)
- requires 0 <= N && A != null && B != null && N == |A| && N == |B| && A != B;
+ requires 0 <= N && A != null && B != null && N == A.Length && N == B.Length && A != B;
requires (forall k :: 0 <= k && k < N ==> 0 <= A[k] && A[k] < N);
requires (forall j,k :: 0 <= j && j < k && k < N ==> A[j] != A[k]); // A is injective
requires (forall m :: 0 <= m && m < N && inImage(m) ==> (exists k :: 0 <= k && k < N && A[k] == m)); // A is surjective
@@ -72,7 +72,7 @@ method PrintArray(a: array<int>) requires a != null;
{
var i := 0;
- while (i < |a|) {
+ while (i < a.Length) {
print a[i], "\n";
i := i + 1;
}
|