blob: 2f9c4bbdf49d263df119650fc641fa476690786f (
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method test(x:seq<int>)
requires |x| == 10;
{
var elts := x[4:2:3];
var a, b, c := elts[0], elts[1], elts[2];
assert |a| == 4;
assert |b| == 2;
assert |c| == 3;
assert forall i :: 0 <= i < |a| ==> a[i] == x[i];
assert forall i :: 0 <= i < |b| ==> b[i] == x[i+4];
assert forall i :: 0 <= i < |c| ==> c[i] == x[i+6];
var elts2 := x[1:5:]; // Leaving off the last length puts the remaining elements in the last seq
var d, e, f := elts2[0], elts2[1], elts2[2];
assert |d| == 1;
assert |e| == 5;
assert |f| == |x| - (|d| + |e|);
assert forall i :: 0 <= i < |d| ==> d[i] == x[i];
assert forall i :: 0 <= i < |e| ==> e[i] == x[i+1];
assert forall i :: 0 <= i < |f| ==> f[i] == x[i+6];
}
newtype MyNumeric = n | 0 <= n < 100
method NumericSlice<T>(x: seq<T>, two: MyNumeric) returns (y: seq<T>)
requires 10 <= |x| && two == 2;
ensures |y| == 3;
{
var slices;
if * {
slices := x[0:two:3:0:];
} else {
slices := x[1 : 1 : 1 : 3 : two : two : 0];
assert |slices[5]| == 2;
}
assert |slices| == 5 || |slices| == 7;
return middle(slices);
}
function method middle<G>(s: seq<G>): G
requires |s| % 2 == 1;
{
s[|s| / 2]
}
|