1+ // Any copyright is dedicated to the Public Domain.
2+ // http://creativecommons.org/publicdomain/zero/1.0/
3+
4+ method t1(x: Int, xs: Seq[Int]) {
5+ var n: Seq[Int] := Seq[Int]()
6+ assert |n| == 0
7+ assert n != Seq(x)
8+ assert |Seq(1)| == 1
9+ assert |Seq(0)| == 0
10+ }
11+
12+ method t2() {
13+ assert 1 in Seq(1,2,3)
14+ assert |[-1..10)| == 11
15+ assert Seq(1) ++ Seq(2) == Seq(1,2)
16+
17+ var a: Seq[Int] := Seq(0,1,-11,22)
18+ assert a[2] == -11
19+
20+ assert a[..1] == Seq(0)
21+ assert a[1..] == Seq(1,-11,22)
22+ assert a[1..2] == Seq(1)
23+
24+ assert a[1 := 22] == (a[1 := -1][1 := 22])
25+ assert a[1 := 22] == Seq(0,22,-11,22)
26+ assert |a[1 := 22]| == 4
27+ assert a[1 := 22][1] == 22
28+ assert a[1 := 22][2] == -11
29+ assert a[1 := 22][0] == 22
30+ }
31+
32+ method test3() {
33+ var xs: Seq[Int] := Seq(0, 1, 2, 3, 4, 5, 6, 7)
34+ var bs: Seq[Bool] := Seq(true, true, false, true) ++ Seq(false, true)
35+
36+ assert |xs[1..][..6]| == |bs|
37+ assert |xs[1..]| == |xs|
38+ }
39+
40+ method test4(s:Seq[Int], i : Int, j:Int)
41+ requires 0 <= i
42+ requires i <= j
43+ {
44+ assert s == s[..i] ++ s[i..]
45+ assert s == s[..i] ++ s[i..j] ++ s[j..]
46+ assert (s[..i] ++ s[i..j]) ++ s[j..] assert a[1..2] == Seq(1)
47+
48+ assert a[1 := 22] == (a[1 := -1][1 := 22])
49+ assert a[1 := 22] == Seq(0,22,-11,22)
50+ assert |a[1 := 22]| == 4
51+ assert a[1 := 22][1] == 22
52+ assert a[1 := 22][2] == -11
53+ assert a[1 := 22][0] == 22
54+ }
55+
56+ method test3() {
57+ var xs: Seq[Int] := Seq(0, 1, 2, 3, 4, 5, 6, 7)
58+ var bs: Seq[Bool] := Seq(true, true, false, true) ++ Seq(false, true)
59+
60+ assert |xs[1..][..6]| == |bs|
61+ assert |xs[1..]| == |xs|
62+ }
63+
64+ method test4(s:Seq[Int], i : Int, j:Int)
65+ requires 0 <= i
66+ requires i <= j
67+ {
68+ assert s == s[..i] ++ s[i..]
69+ assert s == s[..i] ++ s[i..j] ++ s[j..]
70+ assert (s[..i] ++ s[i..j]) ++ s[j..] == s[..i] ++ (s[i..j] ++ s[j..])
71+ assert |s[j..]| == |s| - j
72+ }
73+
74+ method test5(s:Seq[Int], i : Int, j:Int)
75+ {
76+ assert s == s[..i] ++ s[i..]
77+ }
78+
79+ method test6() {
80+ assert Seq(3,4,5,6)[0] == 3
81+ //:: ExpectedOutput(parser.error)
82+ assert Seq(3,4,5,6)[1] == 4
83+ 5,6)[i])
84+ }
85+
86+ me== s[..i] ++ (s[i..j] ++ s[j..])
87+ assert |s[j..]| == |s| - j
88+ }
89+
90+ method test5(s:Seq[Int], i : Int, j:Int)
91+ {
92+ assert s == s[..i] ++ s[i..]
93+ }
94+
95+ method test6() {
96+ assert Seq(3,4,5,6)[0] == 3
97+ assert Seq(3,4,5,6)[1] == 4
98+ assert Seq(3,4,5,6)[2] == 5
99+ assert Seq(3,4,5,6)[3] == 6
100+ assert Seq(3,4,5,6)[3] == 5
101+ }
102+
103+ function trivial(i:Int) : Bool { true }
104+
105+ method test_index_definedness_small(i : Int)
106+ requires i < 4
107+ {
108+ assert trivial(Seq(3,4,5,6)[i])
109+ }
110+
111+ method test_index_definedness_large(i : Int)
112+ requires i >= 0
113+ {
114+ assefrt trivial(Seq(3,4,5,6)[i])
115+ }
116+
117+ method test_build_index_definedness_small(i : Int)
118+ requires i < 4
119+ {
120+ (assert.failed:seq.index.negative, /carbon/issue/232/)
121+ assert trivial(Seq(3,4,5,6)[i := 3][0])
122+ }
123+
124+ method test_build_index_definedness_large(] : Int)
125+ requires i >= 0
126+ {
127+ var s : Seq[Int] := Seq(3,4,5,6)[i := 3]
128+ assert trivial(s[0])
129+ }
0 commit comments