/[eiffelstudio]/branches/eth/eve/Src/library/base/mml/sequence.bpl
ViewVC logotype

Contents of /branches/eth/eve/Src/library/base/mml/sequence.bpl

Parent Directory Parent Directory | Revision Log Revision Log


Revision 94771 - (show annotations)
Thu Apr 3 12:37:44 2014 UTC (5 years, 6 months ago) by polikarn
File size: 12266 byte(s)
Bugfix: redefinitions now taken into account when calculating replaced model queries.
1 // Finite sequences.
2 // (Originally from Dafny Prelude: Copyright (c) Microsoft)
3
4 // Sequence type
5 type Seq T;
6
7 // Sequence length
8 function Seq#Length<T>(Seq T): int;
9 axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
10
11 // Empty sequence
12 function Seq#Empty<T>(): Seq T;
13 axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
14 axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
15 axiom (forall<T> f: Field (Seq T) :: { Default(f) } Default(f) == Seq#Empty());
16
17 // Singleton sequence
18 function Seq#Singleton<T>(T): Seq T;
19 axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
20
21 // Does a sequence contain a given element?
22 function Seq#Has<T>(s: Seq T, x: T): bool;
23 axiom (forall<T> s: Seq T, x: T :: { Seq#Has(s,x) }
24 Seq#Has(s,x) <==>
25 (exists i: int :: { Seq#Item(s,i) } 1 <= i && i <= Seq#Length(s) && Seq#Item(s,i) == x));
26 axiom (forall<T> s: Seq T, i: int :: { Seq#Item(s,i) }
27 1 <= i && i <= Seq#Length(s) ==>
28 Seq#Has(s, Seq#Item(s, i)));
29 axiom (forall<T> x: T ::
30 { Seq#Has(Seq#Empty(), x) }
31 !Seq#Has(Seq#Empty(), x));
32 axiom (forall<T> x, y: T ::
33 { Seq#Has(Seq#Singleton(y), x) }
34 Seq#Has(Seq#Singleton(y), x) <==> x == y);
35 axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
36 { Seq#Has(Seq#Concat(s0, s1), x) }
37 Seq#Has(Seq#Concat(s0, s1), x) <==>
38 Seq#Has(s0, x) || Seq#Has(s1, x));
39 axiom (forall<T> s: Seq T, v: T, x: T ::
40 { Seq#Has(Seq#Extended(s, v), x) }
41 Seq#Has(Seq#Extended(s, v), x) <==> (v == x || Seq#Has(s, x)));
42 axiom (forall<T> s: Seq T, n: int, x: T ::
43 { Seq#Has(Seq#Take(s, n), x) }
44 Seq#Has(Seq#Take(s, n), x) <==>
45 (exists i: int :: { Seq#Item(s, i) }
46 1 <= i && i <= n && i <= Seq#Length(s) && Seq#Item(s, i) == x));
47 axiom (forall<T> s: Seq T, n: int, x: T ::
48 { Seq#Has(Seq#Drop(s, n), x) }
49 Seq#Has(Seq#Drop(s, n), x) <==>
50 (exists i: int :: { Seq#Item(s, i) }
51 0 <= n && n + 1 <= i && i <= Seq#Length(s) && Seq#Item(s, i) == x));
52
53 // Is a sequence empty?
54 function {: inline } Seq#IsEmpty<T>(a: Seq T): bool
55 { Seq#Equal(a, Seq#Empty()) }
56
57 // Element at a given index
58 function Seq#Item<T>(Seq T, int): T;
59 axiom (forall<T> t: T :: { Seq#Item(Seq#Singleton(t), 1) } Seq#Item(Seq#Singleton(t), 1) == t);
60 axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Item(Seq#Concat(s0,s1), n) }
61 (n <= Seq#Length(s0) ==> Seq#Item(Seq#Concat(s0,s1), n) == Seq#Item(s0, n)) &&
62 (Seq#Length(s0) < n ==> Seq#Item(Seq#Concat(s0,s1), n) == Seq#Item(s1, n - Seq#Length(s0))));
63
64 // Set of indexes
65 function Seq#Domain<T>(q: Seq T): Set int
66 { Interval#FromRange(1, Seq#Length(q)) }
67
68 // Set of values
69 function Seq#Range<T>(Seq T): Set T;
70 axiom (forall<T> q: Seq T, o: T :: { Seq#Range(q)[o] }{ Seq#Has(q, o) } Seq#Has(q, o) <==> Seq#Range(q)[o]);
71
72 // How many times does x occur in a?
73 function Seq#Occurrences<T>(Seq T, T): int;
74 axiom (forall<T> x: T :: {Seq#Occurrences(Seq#Empty(), x)} Seq#Occurrences(Seq#Empty(), x) == 0);
75 axiom (forall<T> a: Seq T, x: T:: {Seq#Occurrences(Seq#Extended(a, x), x)}
76 Seq#Occurrences(Seq#Extended(a, x), x) == Seq#Occurrences(a, x) + 1);
77 axiom (forall<T> a: Seq T, x: T, y: T :: {Seq#Occurrences(Seq#Extended(a, y), x)}
78 x != y ==> Seq#Occurrences(Seq#Extended(a, y), x) == Seq#Occurrences(a, x));
79
80 // Are two sequences equal?
81 function Seq#Equal<T>(Seq T, Seq T): bool;
82 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
83 Seq#Equal(s0,s1) <==>
84 Seq#Length(s0) == Seq#Length(s1) &&
85 (forall j: int :: { Seq#Item(s0,j) } { Seq#Item(s1,j) }
86 1 <= j && j <= Seq#Length(s0) ==> Seq#Item(s0,j) == Seq#Item(s1,j)));
87 axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
88 Seq#Equal(a,b) ==> a == b);
89
90 // Is q0 a prefix of q1?
91 function {: inline } Seq#Prefix<T>(q0: Seq T, q1: Seq T): bool
92 { Seq#Equal(q0, Seq#Take(q1, Seq#Length(q0))) }
93
94 // Is |q0| <= |q1|?
95 function {: inline } Seq#LessEqual<T>(q0: Seq T, q1: Seq T): bool
96 { Seq#Length(q0) <= Seq#Length(q1) }
97
98 // Prefix of length how_many
99 function Seq#Take<T>(s: Seq T, howMany: int): Seq T;
100 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
101 0 <= n ==>
102 (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
103 (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
104 axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Item(Seq#Take(s,n), j) } {:weight 25}
105 1 <= j && j <= n && j <= Seq#Length(s) ==>
106 Seq#Item(Seq#Take(s,n), j) == Seq#Item(s, j));
107
108 // Sequence without its prefix of length howMany
109 function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;
110 axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
111 0 <= n ==>
112 (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
113 (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
114 axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Item(Seq#Drop(s,n), j) } {:weight 25}
115 0 <= n && 1 <= j && j <= Seq#Length(s)-n ==>
116 Seq#Item(Seq#Drop(s,n), j) == Seq#Item(s, j+n));
117
118 // First element
119 function {: inline } Seq#First<T>(q: Seq T): T
120 { Seq#Item(q, 1) }
121
122 // Last element
123 function {: inline } Seq#Last<T>(q: Seq T): T
124 { Seq#Item(q, Seq#Length(q)) }
125
126 // Sequence with the first element removed
127 function {: inline } Seq#ButFirst<T>(q: Seq T): Seq T
128 { Seq#Drop(q, 1) }
129
130 // Sequence with the last element removed
131 function {: inline } Seq#ButLast<T>(q: Seq T): Seq T
132 { Seq#Take(q, Seq#Length(q) - 1) }
133
134 // Prefix until upper
135 function {: inline } Seq#Front<T>(q: Seq T, upper: int): Seq T
136 { if 0 <= upper then Seq#Take(q, upper) else Seq#Empty() }
137
138 // Suffix from lower
139 function {: inline } Seq#Tail<T>(q: Seq T, lower: int): Seq T
140 { if 1 <= lower then Seq#Drop(q, lower - 1) else q }
141
142 // Subsequence from lower to upper
143 function {: inline } Seq#Interval<T>(q: Seq T, lower: int, upper: int): Seq T
144 { Seq#Tail(Seq#Front(q, upper), lower) }
145
146 // Sequence with element at position i removed
147 function {: inline } Seq#RemovedAt<T>(q: Seq T, i: int): Seq T
148 { Seq#Concat(Seq#Take(q, i - 1), Seq#Drop(q, i)) }
149
150 // Sequence extended with x at the end
151 function Seq#Extended<T>(s: Seq T, val: T): Seq T;
152 axiom (forall<T> s: Seq T, v: T :: { Seq#Length(Seq#Extended(s,v)) }
153 Seq#Length(Seq#Extended(s,v)) == 1 + Seq#Length(s));
154 axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Item(Seq#Extended(s,v), i) }
155 (i == Seq#Length(s) + 1 ==> Seq#Item(Seq#Extended(s,v), i) == v) &&
156 (i <= Seq#Length(s) ==> Seq#Item(Seq#Extended(s,v), i) == Seq#Item(s, i)));
157
158 // Sequence with x inserted at position i
159 function {: inline } Seq#ExtendedAt<T>(s: Seq T, i: int, val: T): Seq T
160 {
161 Seq#Concat (Seq#Extended(Seq#Take(s, i - 1), val), Seq#Drop(s, i -1))
162 }
163
164 // Sequence prepended with x at the beginning
165 function Seq#Prepended<T>(s: Seq T, val: T): Seq T
166 {
167 Seq#Concat (Seq#Singleton(val), s)
168 }
169 axiom (forall<T> s: Seq T, val: T, i: int :: { Seq#Item(Seq#Prepended(s, val), i) }
170 2 <= i && i <= Seq#Length(s) + 1 ==> Seq#Item(Seq#Prepended(s, val), i) == Seq#Item(s, i - 1));
171 axiom (forall<T> s: Seq T, val: T :: { Seq#Item(Seq#Prepended(s, val), 1) }
172 Seq#Item(Seq#Prepended(s, val), 1) == val);
173
174 // Concatenation of two sequences
175 function Seq#Concat<T>(Seq T, Seq T): Seq T;
176 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Concat(s0,s1)) }
177 Seq#Length(Seq#Concat(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
178
179 // Sequence with x at position i.
180 function Seq#Update<T>(Seq T, int, T): Seq T;
181 axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
182 1 <= i && i <= Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
183 axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Item(Seq#Update(s,i,v),n) }
184 1 <= n && n <= Seq#Length(s) ==>
185 (i == n ==> Seq#Item(Seq#Update(s,i,v),n) == v) &&
186 (i != n ==> Seq#Item(Seq#Update(s,i,v),n) == Seq#Item(s,n)));
187
188 // Sequence converted to a bag
189 function Seq#ToBag<T>(Seq T): Bag T;
190 axiom (forall<T> s: Seq T :: { Seq#ToBag(s) } Bag#IsValid(Seq#ToBag(s)));
191 // building axiom
192 axiom (forall<T> s: Seq T, v: T ::
193 { Seq#ToBag(Seq#Extended(s, v)) }
194 Seq#ToBag(Seq#Extended(s, v)) == Bag#Extended(Seq#ToBag(s), v)
195 );
196 axiom (forall<T> :: Seq#ToBag(Seq#Empty(): Seq T) == Bag#Empty(): Bag T);
197 axiom (forall<T> s: Seq T :: { Bag#Card(Seq#ToBag(s)) }
198 Bag#Card(Seq#ToBag(s)) == Seq#Length(s));
199
200 // concatenation axiom
201 axiom (forall<T> a: Seq T, b: Seq T ::
202 { Seq#ToBag(Seq#Concat(a, b)) }
203 Seq#ToBag(Seq#Concat(a, b)) == Bag#Union(Seq#ToBag(a), Seq#ToBag(b)) );
204
205 // update axiom
206 axiom (forall<T> s: Seq T, i: int, v: T, x: T ::
207 { Seq#ToBag(Seq#Update(s, i, v))[x] }
208 0 <= i && i < Seq#Length(s) ==>
209 Seq#ToBag(Seq#Update(s, i, v))[x] ==
210 Bag#Union(Bag#Difference(Seq#ToBag(s), Bag#Singleton(Seq#Item(s,i))), Bag#Singleton(v))[x] );
211 // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}}
212 axiom (forall<T> s: Seq T, x: T :: { Seq#ToBag(s)[x] } Seq#Has(s, x) <==> 0 < Seq#ToBag(s)[x]);
213 axiom (forall<T> s: Seq T, x: T :: { Seq#ToBag(s)[x] } Seq#ToBag(s)[x] == Seq#Occurrences(s, x));
214
215 // Sequence converted to map
216 function Seq#ToMap<T>(Seq T): Map int T;
217 axiom (forall<T> s: Seq T :: { Seq#ToMap(s) }
218 Map#Equal(Seq#ToMap(s), Map#Empty()) <==> Seq#Equal (s, Seq#Empty()));
219 axiom (forall<T> s: Seq T :: { Map#Domain(Seq#ToMap(s)) }
220 Map#Domain(Seq#ToMap(s)) == Seq#Domain(s));
221 axiom (forall<T> s: Seq T :: { Map#Card(Seq#ToMap(s)) }
222 Map#Card(Seq#ToMap(s)) == Seq#Length(s));
223 axiom (forall<T> s: Seq T, i: int :: { Map#Item(Seq#ToMap(s), i) }
224 1 <= i && i <= Seq#Length(s) ==> Map#Item(Seq#ToMap(s), i) == Seq#Item(s, i));
225
226 axiom (forall<T> s: Seq T :: { Map#ToBag(Seq#ToMap(s)) }
227 Bag#Equal(Map#ToBag(Seq#ToMap(s)), Seq#ToBag(s)));
228
229
230 // Additional axioms about common things
231
232 axiom (forall<T> s, t: Seq T ::
233 { Seq#Concat(s, t) }
234 Seq#Take(Seq#Concat(s, t), Seq#Length(s)) == s &&
235 Seq#Drop(Seq#Concat(s, t), Seq#Length(s)) == t);
236
237 // Commutability of Take and Drop with Update.
238 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
239 { Seq#Take(Seq#Update(s, i, v), n) }
240 1 <= i && i <= n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
241 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
242 { Seq#Take(Seq#Update(s, i, v), n) }
243 n < i && i <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
244 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
245 { Seq#Drop(Seq#Update(s, i, v), n) }
246 0 <= n && n + 1 <= i && i <= Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
247 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
248 { Seq#Drop(Seq#Update(s, i, v), n) }
249 1 <= i && i <= n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
250 // drop commutes with build.
251 axiom (forall<T> s: Seq T, v: T, n: int ::
252 { Seq#Drop(Seq#Extended(s, v), n) }
253 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Extended(s, v), n) == Seq#Extended(Seq#Drop(s, n), v) );
254
255 axiom Seq#Take(Seq#Empty(), 0) == Seq#Empty(); // [][..0] == []
256 axiom Seq#Drop(Seq#Empty(), 0) == Seq#Empty(); // [][0..] == []
257
258
259 function Seq#IsSorted<T>(s: Seq T) returns (bool);
260
261 //axiom (forall s: Seq int, i: int ::
262 // 1 <= i && i < Seq#Length(s) && Seq#IsSorted(s) ==> Seq#Item(s, i) <= Seq#Item(s, i+1));
263 axiom (forall s: Seq int ::
264 { Seq#IsSorted(s) }
265 Seq#IsSorted(s) ==> (forall i, j: int :: 1 <= i && i <= Seq#Length(s) && i <= j && j <= Seq#Length(s) ==> Seq#Item(s, i) <= Seq#Item(s, j)));
266 axiom (forall s: Seq int ::
267 { Seq#IsSorted(s) }
268 Seq#Length(s) <= 1 ==> Seq#IsSorted(s));
269 axiom (forall s: Seq int, i: int ::
270 1 <= i && i < Seq#Length(s) && Seq#IsSorted(Seq#Front(s, i)) && Seq#Item(s, i) <= Seq#Item(s, i+1) ==> Seq#IsSorted(Seq#Front(s, i+1)));
271
272 axiom (forall s: Seq int ::
273 { Seq#Range(s) }
274 (forall i: int, j: int ::
275 1 <= i && i < Seq#Length(s) && 1 <= j && j < Seq#Length(s) ==>
276 Seq#Range(Seq#Update(Seq#Update(s, i, Seq#Item(s, j)), j, Seq#Item(s, i))) == Seq#Range(s)));
277
278
279
280

  ViewVC Help
Powered by ViewVC 1.1.23