blob: aa131f9817ccfded55804bc6c1e452fd8049a13a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method Main() { }
method H(a: array<int>, c: array<int>, n: nat, j: nat)
requires a != null && c != null
requires j < n == a.Length == c.Length
{
var A := a[..];
var C := c[..];
if {
case A[j] == C[j] =>
assert a[j] == c[j];
case forall i :: 0 <= i < n ==> A[i] == C[i] =>
assert a[j] == c[j];
case forall i :: 0 <= i < n ==> A[i] == C[i] =>
assert forall i :: 0 <= i < n ==> a[i] == c[i];
case A == C =>
assert forall i :: 0 <= i < n ==> A[i] == C[i];
case A == C =>
assert forall i :: 0 <= i < n ==> a[i] == c[i];
case true =>
}
}
method K(a: array<int>, c: array<int>, n: nat)
requires a != null && c != null
requires n <= a.Length && n <= c.Length
{
var A := a[..n];
var C := c[..n];
if {
case A == C =>
assert forall i :: 0 <= i < n ==> A[i] == C[i];
case A == C =>
assert forall i :: 0 <= i < n ==> a[i] == c[i];
case true =>
}
}
method L(a: array<int>, c: array<int>, n: nat)
requires a != null && c != null
requires n <= a.Length == c.Length
{
var A := a[n..];
var C := c[n..];
var h := a.Length - n;
if {
case A == C =>
assert forall i :: 0 <= i < h ==> A[i] == C[i];
case A == C =>
assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];
case true =>
}
}
method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
requires a != null && c != null
requires k + m <= a.Length
requires l + n <= c.Length
{
if {
case true =>
var A := a[k..k+m];
var C := c[l..l+n];
if A == C {
if * {
assert m == n;
} else if * {
assert forall i :: 0 <= i < n ==> A[i] == C[i];
} else if * {
assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];
} else if * {
assert forall i :: 0 <= i < n ==> A[i] == a[k+i];
} else if * {
assert forall i :: 0 <= i < n ==> C[i] == c[l+i];
} else if * {
assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];
}
}
case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
assert a[..m] == c[l..l+m];
case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>
assert a[k..] == c[l+k..l+a.Length];
case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>
assert a[k..k+m] == c[l+k..l+k+m];
}
}
|
