1
2 // Copyright (C) 2008-2018 Lorenzo Caminiti
3 // Distributed under the Boost Software License, Version 1.0 (see accompanying
4 // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
5 // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
6
7 //[n1962_vector
8 #include <boost/contract.hpp>
9 #include <boost/bind.hpp>
10 #include <boost/optional.hpp>
11 #include <boost/algorithm/cxx11/all_of.hpp>
12 #include <boost/type_traits/has_equal_to.hpp>
13 #include <boost/next_prior.hpp>
14 #include <vector>
15 #include <functional>
16 #include <iterator>
17 #include <memory>
18 #include <cassert>
19
20 // Could be programmed at call site with C++14 generic lambdas.
21 struct all_of_equal_to {
22 typedef bool result_type;
23
24 template<typename InputIter, typename T>
operator ()all_of_equal_to25 result_type operator()(InputIter first, InputIter last, T const& value) {
26 return boost::algorithm::all_of_equal(first, last, value);
27 }
28
29 template<typename InputIter>
operator ()all_of_equal_to30 result_type operator()(InputIter first, InputIter last, InputIter where) {
31 for(InputIter i = first, j = where; i != last; ++i, ++j) {
32 if(*i != *j) return false;
33 }
34 return true;
35 }
36 };
37
38 template<typename Iter>
39 bool valid(Iter first, Iter last); // Cannot implement in C++ (for axiom only).
40
41 template<typename Iter>
42 bool contained(Iter first1, Iter last1, Iter first2, Iter last2); // For axiom.
43
44 // STL vector requires T copyable but not equality comparable.
45 template<typename T, class Allocator = std::allocator<T> >
46 class vector {
47 friend class boost::contract::access;
48
invariant() const49 void invariant() const {
50 BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
51 BOOST_CONTRACT_ASSERT(std::distance(begin(), end()) == int(size()));
52 BOOST_CONTRACT_ASSERT(std::distance(rbegin(), rend()) == int(size()));
53 BOOST_CONTRACT_ASSERT(size() <= capacity());
54 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
55 }
56
57 public:
58 typedef typename std::vector<T, Allocator>::allocator_type allocator_type;
59 typedef typename std::vector<T, Allocator>::pointer pointer;
60 typedef typename std::vector<T, Allocator>::const_pointer const_pointer;
61 typedef typename std::vector<T, Allocator>::reference reference;
62 typedef typename std::vector<T, Allocator>::const_reference const_reference;
63 typedef typename std::vector<T, Allocator>::value_type value_type;
64 typedef typename std::vector<T, Allocator>::iterator iterator;
65 typedef typename std::vector<T, Allocator>::const_iterator const_iterator;
66 typedef typename std::vector<T, Allocator>::size_type size_type;
67 typedef typename std::vector<T, Allocator>::difference_type difference_type;
68 typedef typename std::vector<T, Allocator>::reverse_iterator
69 reverse_iterator;
70 typedef typename std::vector<T, Allocator>::const_reverse_iterator
71 const_reverse_iterator;
72
vector()73 vector() : vect_() {
74 boost::contract::check c = boost::contract::constructor(this)
75 .postcondition([&] {
76 BOOST_CONTRACT_ASSERT(empty());
77 })
78 ;
79 }
80
vector(Allocator const & alloc)81 explicit vector(Allocator const& alloc) : vect_(alloc) {
82 boost::contract::check c = boost::contract::constructor(this)
83 .postcondition([&] {
84 BOOST_CONTRACT_ASSERT(empty());
85 BOOST_CONTRACT_ASSERT(get_allocator() == alloc);
86 })
87 ;
88 }
89
vector(size_type count)90 explicit vector(size_type count) : vect_(count) {
91 boost::contract::check c = boost::contract::constructor(this)
92 .postcondition([&] {
93 BOOST_CONTRACT_ASSERT(size() == count);
94 BOOST_CONTRACT_ASSERT(
95 boost::contract::condition_if<boost::has_equal_to<T> >(
96 boost::bind(all_of_equal_to(), begin(), end(), T())
97 )
98 );
99 })
100 ;
101 }
102
vector(size_type count,T const & value)103 vector(size_type count, T const& value) : vect_(count, value) {
104 boost::contract::check c = boost::contract::constructor(this)
105 .postcondition([&] {
106 BOOST_CONTRACT_ASSERT(size() == count);
107 BOOST_CONTRACT_ASSERT(
108 boost::contract::condition_if<boost::has_equal_to<T> >(
109 boost::bind(all_of_equal_to(), begin(), end(),
110 boost::cref(value))
111 )
112 );
113 })
114 ;
115 }
116
vector(size_type count,T const & value,Allocator const & alloc)117 vector(size_type count, T const& value, Allocator const& alloc) :
118 vect_(count, value, alloc) {
119 boost::contract::check c = boost::contract::constructor(this)
120 .postcondition([&] {
121 BOOST_CONTRACT_ASSERT(size() == count);
122 BOOST_CONTRACT_ASSERT(
123 boost::contract::condition_if<boost::has_equal_to<T> >(
124 boost::bind(all_of_equal_to(), begin(), end(),
125 boost::cref(value))
126 )
127 );
128 BOOST_CONTRACT_ASSERT(get_allocator() == alloc);
129 })
130 ;
131 }
132
133 template<typename InputIter>
vector(InputIter first,InputIter last)134 vector(InputIter first, InputIter last) : vect_(first, last) {
135 boost::contract::check c = boost::contract::constructor(this)
136 .postcondition([&] {
137 BOOST_CONTRACT_ASSERT(std::distance(first, last) ==
138 int(size()));
139 })
140 ;
141 }
142
143 template<typename InputIter>
vector(InputIter first,InputIter last,Allocator const & alloc)144 vector(InputIter first, InputIter last, Allocator const& alloc) :
145 vect_(first, last, alloc) {
146 boost::contract::check c = boost::contract::constructor(this)
147 .postcondition([&] {
148 BOOST_CONTRACT_ASSERT(std::distance(first, last) ==
149 int(size()));
150 BOOST_CONTRACT_ASSERT(get_allocator() == alloc);
151 })
152 ;
153 }
154
vector(vector const & other)155 /* implicit */ vector(vector const& other) : vect_(other.vect_) {
156 boost::contract::check c = boost::contract::constructor(this)
157 .postcondition([&] {
158 BOOST_CONTRACT_ASSERT(
159 boost::contract::condition_if<boost::has_equal_to<T> >(
160 boost::bind(std::equal_to<vector<T> >(),
161 boost::cref(*this), boost::cref(other))
162 )
163 );
164 })
165 ;
166 }
167
operator =(vector const & other)168 vector& operator=(vector const& other) {
169 boost::optional<vector&> result;
170 boost::contract::check c = boost::contract::public_function(this)
171 .postcondition([&] {
172 BOOST_CONTRACT_ASSERT(
173 boost::contract::condition_if<boost::has_equal_to<T> >(
174 boost::bind(std::equal_to<vector<T> >(),
175 boost::cref(*this), boost::cref(other))
176 )
177 );
178 BOOST_CONTRACT_ASSERT(
179 boost::contract::condition_if<boost::has_equal_to<T> >(
180 boost::bind(std::equal_to<vector<T> >(),
181 boost::cref(*result), boost::cref(*this))
182 )
183 );
184 })
185 ;
186
187 if(this != &other) vect_ = other.vect_;
188 return *(result = *this);
189 }
190
~vector()191 virtual ~vector() {
192 // Check invariants.
193 boost::contract::check c = boost::contract::destructor(this);
194 }
195
reserve(size_type count)196 void reserve(size_type count) {
197 boost::contract::check c = boost::contract::public_function(this)
198 .precondition([&] {
199 BOOST_CONTRACT_ASSERT(count < max_size());
200 })
201 .postcondition([&] {
202 BOOST_CONTRACT_ASSERT(capacity() >= count);
203 })
204 ;
205
206 vect_.reserve(count);
207 }
208
capacity() const209 size_type capacity() const {
210 size_type result;
211 boost::contract::check c = boost::contract::public_function(this)
212 .postcondition([&] {
213 BOOST_CONTRACT_ASSERT(result >= size());
214 })
215 ;
216
217 return result = vect_.capacity();
218 }
219
begin()220 iterator begin() {
221 iterator result;
222 boost::contract::check c = boost::contract::public_function(this)
223 .postcondition([&] {
224 if(empty()) BOOST_CONTRACT_ASSERT(result == end());
225 })
226 ;
227
228 return result = vect_.begin();
229 }
230
begin() const231 const_iterator begin() const {
232 const_iterator result;
233 boost::contract::check c = boost::contract::public_function(this)
234 .postcondition([&] {
235 if(empty()) BOOST_CONTRACT_ASSERT(result == end());
236 })
237 ;
238
239 return result = vect_.begin();
240 }
241
end()242 iterator end() {
243 // Check invariants.
244 boost::contract::check c = boost::contract::public_function(this);
245 return vect_.end();
246 }
247
end() const248 const_iterator end() const {
249 // Check invariants.
250 boost::contract::check c = boost::contract::public_function(this);
251 return vect_.end();
252 }
253
rbegin()254 reverse_iterator rbegin() {
255 iterator result;
256 boost::contract::check c = boost::contract::public_function(this)
257 .postcondition([&] {
258 if(empty()) BOOST_CONTRACT_ASSERT(result == rend());
259 })
260 ;
261
262 return result = vect_.rbegin();
263 }
264
rbegin() const265 const_reverse_iterator rbegin() const {
266 const_reverse_iterator result;
267 boost::contract::check c = boost::contract::public_function(this)
268 .postcondition([&] {
269 if(empty()) BOOST_CONTRACT_ASSERT(result == rend());
270 })
271 ;
272
273 return result = vect_.rbegin();
274 }
275
rend()276 reverse_iterator rend() {
277 // Check invariants.
278 boost::contract::check c = boost::contract::public_function(this);
279 return vect_.rend();
280 }
281
rend() const282 const_reverse_iterator rend() const {
283 // Check invariants.
284 boost::contract::check c = boost::contract::public_function(this);
285 return vect_.rend();
286 }
287
resize(size_type count,T const & value=T ())288 void resize(size_type count, T const& value = T()) {
289 boost::contract::old_ptr<size_type> old_size =
290 BOOST_CONTRACT_OLDOF(size());
291 boost::contract::check c = boost::contract::public_function(this)
292 .postcondition([&] {
293 BOOST_CONTRACT_ASSERT(size() == count);
294 if(count > *old_size) {
295 BOOST_CONTRACT_ASSERT(
296 boost::contract::condition_if<boost::has_equal_to<T> >(
297 boost::bind(all_of_equal_to(), begin() + *old_size,
298 end(), boost::cref(value))
299 )
300 );
301 }
302 })
303 ;
304
305 vect_.resize(count, value);
306 }
307
size() const308 size_type size() const {
309 size_type result;
310 boost::contract::check c = boost::contract::public_function(this)
311 .postcondition([&] {
312 BOOST_CONTRACT_ASSERT(result <= capacity());
313 })
314 ;
315
316 return result = vect_.size();
317 }
318
max_size() const319 size_type max_size() const {
320 size_type result;
321 boost::contract::check c = boost::contract::public_function(this)
322 .postcondition([&] {
323 BOOST_CONTRACT_ASSERT(result >= capacity());
324 })
325 ;
326
327 return result = vect_.max_size();
328 }
329
empty() const330 bool empty() const {
331 bool result;
332 boost::contract::check c = boost::contract::public_function(this)
333 .postcondition([&] {
334 BOOST_CONTRACT_ASSERT(result == (size() == 0));
335 })
336 ;
337
338 return result = vect_.empty();
339 }
340
get_allocator() const341 Allocator get_allocator() const {
342 // Check invariants.
343 boost::contract::check c = boost::contract::public_function(this);
344 return vect_.get_allocator();
345 }
346
at(size_type index)347 reference at(size_type index) {
348 // Check invariants, no pre (throw out_of_range for invalid index).
349 boost::contract::check c = boost::contract::public_function(this);
350 return vect_.at(index);
351 }
352
at(size_type index) const353 const_reference at(size_type index) const {
354 // Check invariants, no pre (throw out_of_range for invalid index).
355 boost::contract::check c = boost::contract::public_function(this);
356 return vect_.at(index);
357 }
358
operator [](size_type index)359 reference operator[](size_type index) {
360 boost::contract::check c = boost::contract::public_function(this)
361 .precondition([&] {
362 BOOST_CONTRACT_ASSERT(index < size());
363 })
364 ;
365
366 return vect_[index];
367 }
368
operator [](size_type index) const369 const_reference operator[](size_type index) const {
370 boost::contract::check c = boost::contract::public_function(this)
371 .precondition([&] {
372 BOOST_CONTRACT_ASSERT(index < size());
373 })
374 ;
375
376 return vect_[index];
377 }
378
front()379 reference front() {
380 boost::contract::check c = boost::contract::public_function(this)
381 .precondition([&] {
382 BOOST_CONTRACT_ASSERT(!empty());
383 })
384 ;
385
386 return vect_.front();
387 }
388
front() const389 const_reference front() const {
390 boost::contract::check c = boost::contract::public_function(this)
391 .precondition([&] {
392 BOOST_CONTRACT_ASSERT(!empty());
393 })
394 ;
395
396 return vect_.front();
397 }
398
back()399 reference back() {
400 boost::contract::check c = boost::contract::public_function(this)
401 .precondition([&] {
402 BOOST_CONTRACT_ASSERT(!empty());
403 })
404 ;
405
406 return vect_.back();
407 }
408
back() const409 const_reference back() const {
410 boost::contract::check c = boost::contract::public_function(this)
411 .precondition([&] {
412 BOOST_CONTRACT_ASSERT(!empty());
413 })
414 ;
415
416 return vect_.back();
417 }
418
push_back(T const & value)419 void push_back(T const& value) {
420 boost::contract::old_ptr<size_type> old_size =
421 BOOST_CONTRACT_OLDOF(size());
422 boost::contract::old_ptr<size_type> old_capacity =
423 BOOST_CONTRACT_OLDOF(capacity());
424 boost::contract::check c = boost::contract::public_function(this)
425 .precondition([&] {
426 BOOST_CONTRACT_ASSERT(size() < max_size());
427 })
428 .postcondition([&] {
429 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
430 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
431 BOOST_CONTRACT_ASSERT(
432 boost::contract::condition_if<boost::has_equal_to<T> >(
433 boost::bind(std::equal_to<T>(), boost::cref(back()),
434 boost::cref(value))
435 )
436 );
437 })
438 ;
439
440 vect_.push_back(value);
441 }
442
pop_back()443 void pop_back() {
444 boost::contract::old_ptr<size_type> old_size =
445 BOOST_CONTRACT_OLDOF(size());
446 boost::contract::check c = boost::contract::public_function(this)
447 .precondition([&] {
448 BOOST_CONTRACT_ASSERT(!empty());
449 })
450 .postcondition([&] {
451 BOOST_CONTRACT_ASSERT(size() == *old_size - 1);
452 })
453 ;
454
455 vect_.pop_back();
456 }
457
458 template<typename InputIter>
assign(InputIter first,InputIter last)459 void assign(InputIter first, InputIter last) {
460 boost::contract::check c = boost::contract::public_function(this)
461 .precondition([&] {
462 BOOST_CONTRACT_ASSERT_AXIOM(
463 !contained(begin(), end(), first, last));
464 })
465 .postcondition([&] {
466 BOOST_CONTRACT_ASSERT(std::distance(first, last) ==
467 int(size()));
468 })
469 ;
470
471 vect_.assign(first, last);
472 }
473
assign(size_type count,T const & value)474 void assign(size_type count, T const& value) {
475 boost::contract::check c = boost::contract::public_function(this)
476 .precondition([&] {
477 BOOST_CONTRACT_ASSERT(count <= max_size());
478 })
479 .postcondition([&] {
480 BOOST_CONTRACT_ASSERT(
481 boost::contract::condition_if<boost::has_equal_to<T> >(
482 boost::bind(all_of_equal_to(), begin(), end(),
483 boost::cref(value))
484 )
485 );
486 })
487 ;
488
489 vect_.assign(count, value);
490 }
491
insert(iterator where,T const & value)492 iterator insert(iterator where, T const& value) {
493 iterator result;
494 boost::contract::old_ptr<size_type> old_size =
495 BOOST_CONTRACT_OLDOF(size());
496 boost::contract::old_ptr<size_type> old_capacity =
497 BOOST_CONTRACT_OLDOF(capacity());
498 boost::contract::check c = boost::contract::public_function(this)
499 .precondition([&] {
500 BOOST_CONTRACT_ASSERT(size() < max_size());
501 })
502 .postcondition([&] {
503 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
504 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
505 BOOST_CONTRACT_ASSERT(
506 boost::contract::condition_if<boost::has_equal_to<T> >(
507 boost::bind(std::equal_to<T>(), boost::cref(*result),
508 boost::cref(value))
509 )
510 );
511 if(capacity() > *old_capacity) {
512 BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
513 } else {
514 BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
515 }
516 })
517 ;
518
519 return result = vect_.insert(where, value);
520 }
521
insert(iterator where,size_type count,T const & value)522 void insert(iterator where, size_type count, T const& value) {
523 boost::contract::old_ptr<size_type> old_size =
524 BOOST_CONTRACT_OLDOF(size());
525 boost::contract::old_ptr<size_type> old_capacity =
526 BOOST_CONTRACT_OLDOF(capacity());
527 boost::contract::old_ptr<iterator> old_where =
528 BOOST_CONTRACT_OLDOF(where);
529 boost::contract::check c = boost::contract::public_function(this)
530 .precondition([&] {
531 BOOST_CONTRACT_ASSERT(size() + count < max_size());
532 })
533 .postcondition([&] {
534 BOOST_CONTRACT_ASSERT(size() == *old_size + count);
535 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
536 if(capacity() == *old_capacity) {
537 BOOST_CONTRACT_ASSERT(
538 boost::contract::condition_if<boost::has_equal_to<T> >(
539 boost::bind(all_of_equal_to(),
540 boost::prior(*old_where),
541 boost::prior(*old_where) + count,
542 boost::cref(value)
543 )
544 )
545 );
546 BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
547 } else BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
548 })
549 ;
550
551 vect_.insert(where, count, value);
552 }
553
554 template<typename InputIter>
insert(iterator where,InputIter first,InputIter last)555 void insert(iterator where, InputIter first, InputIter last) {
556 boost::contract::old_ptr<size_type> old_size =
557 BOOST_CONTRACT_OLDOF(size());
558 boost::contract::old_ptr<size_type> old_capacity =
559 BOOST_CONTRACT_OLDOF(capacity());
560 boost::contract::old_ptr<iterator> old_where =
561 BOOST_CONTRACT_OLDOF(where);
562 boost::contract::check c = boost::contract::public_function(this)
563 .precondition([&] {
564 BOOST_CONTRACT_ASSERT(size() + std::distance(first, last) <
565 max_size());
566 BOOST_CONTRACT_ASSERT_AXIOM(
567 !contained(first, last, begin(), end()));
568 })
569 .postcondition([&] {
570 BOOST_CONTRACT_ASSERT(size() == *old_size() +
571 std::distance(first, last));
572 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
573 if(capacity() == *old_capacity) {
574 BOOST_CONTRACT_ASSERT(
575 boost::contract::condition_if<boost::has_equal_to<T> >(
576 boost::bind(all_of_equal_to(), first, last,
577 *old_where)
578 )
579 );
580 BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
581 } else BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
582 })
583 ;
584
585 vect_.insert(where, first, last);
586 }
587
erase(iterator where)588 iterator erase(iterator where) {
589 iterator result;
590 boost::contract::old_ptr<size_type> old_size =
591 BOOST_CONTRACT_OLDOF(size());
592 boost::contract::check c = boost::contract::public_function(this)
593 .precondition([&] {
594 BOOST_CONTRACT_ASSERT(!empty());
595 BOOST_CONTRACT_ASSERT(where != end());
596 })
597 .postcondition([&] {
598 BOOST_CONTRACT_ASSERT(size() == *old_size - 1);
599 if(empty()) BOOST_CONTRACT_ASSERT(result == end());
600 BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
601 })
602 ;
603
604 return result = vect_.erase(where);
605 }
606
erase(iterator first,iterator last)607 iterator erase(iterator first, iterator last) {
608 iterator result;
609 boost::contract::old_ptr<size_type> old_size =
610 BOOST_CONTRACT_OLDOF(size());
611 boost::contract::check c = boost::contract::public_function(this)
612 .precondition([&] {
613 BOOST_CONTRACT_ASSERT(size() >= std::distance(first, last));
614 })
615 .postcondition([&] {
616 BOOST_CONTRACT_ASSERT(size() == *old_size -
617 std::distance(first, last));
618 if(empty()) BOOST_CONTRACT_ASSERT(result == end());
619 BOOST_CONTRACT_ASSERT_AXIOM(!valid(first, last));
620 })
621 ;
622
623 return result = vect_.erase(first, last);
624 }
625
clear()626 void clear() {
627 boost::contract::check c = boost::contract::public_function(this)
628 .postcondition([&] {
629 BOOST_CONTRACT_ASSERT(empty());
630 })
631 ;
632
633 vect_.clear();
634 }
635
swap(vector & other)636 void swap(vector& other) {
637 boost::contract::old_ptr<vector> old_me, old_other;
638 #ifdef BOOST_CONTRACT_AUDITS
639 old_me = BOOST_CONTRACT_OLDOF(*this);
640 old_other = BOOST_CONTRACT_OLDOF(other);
641 #endif
642 boost::contract::check c = boost::contract::public_function(this)
643 .precondition([&] {
644 BOOST_CONTRACT_ASSERT(get_allocator() == other.get_allocator());
645 })
646 .postcondition([&] {
647 BOOST_CONTRACT_ASSERT_AUDIT(
648 boost::contract::condition_if<boost::has_equal_to<
649 vector<T> > >(
650 boost::bind(std::equal_to<vector<T> >(),
651 boost::cref(*this), boost::cref(*old_other))
652 )
653 );
654 BOOST_CONTRACT_ASSERT_AUDIT(
655 boost::contract::condition_if<boost::has_equal_to<
656 vector<T> > >(
657 boost::bind(std::equal_to<vector<T> >(),
658 boost::cref(other), boost::cref(*old_me))
659 )
660 );
661 })
662 ;
663
664 vect_.swap(other);
665 }
666
operator ==(vector const & left,vector const & right)667 friend bool operator==(vector const& left, vector const& right) {
668 // Check class invariants for left and right objects.
669 boost::contract::check left_inv =
670 boost::contract::public_function(&left);
671 boost::contract::check right_inv =
672 boost::contract::public_function(&right);
673 return left.vect_ == right.vect_;
674 }
675
676 private:
677 std::vector<T, Allocator> vect_;
678 };
679
main()680 int main() {
681 // char type has operator==.
682
683 vector<char> v(3);
684 assert(v.size() == 3);
685 assert(boost::algorithm::all_of_equal(v, '\0'));
686
687 vector<char> const& cv = v;
688 assert(cv == v);
689
690 vector<char> w(v);
691 assert(w == v);
692
693 typename vector<char>::iterator i = v.begin();
694 assert(*i == '\0');
695
696 typename vector<char>::const_iterator ci = cv.begin();
697 assert(*ci == '\0');
698
699 v.insert(i, 2, 'a');
700 assert(v[0] == 'a');
701 assert(v[1] == 'a');
702
703 v.push_back('b');
704 assert(v.back() == 'b');
705
706 struct x {}; // x type doest not have operator==.
707
708 vector<x> y(3);
709 assert(y.size() == 3);
710
711 vector<x> const& cy = y;
712 vector<x> z(y);
713
714 typename vector<x>::iterator j = y.begin();
715 assert(j != y.end());
716 typename vector<x>::const_iterator cj = cy.begin();
717 assert(cj != cy.end());
718
719 y.insert(j, 2, x());
720 y.push_back(x());
721
722 return 0;
723 }
724 //]
725
726