• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
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 //[cline90_vector_axx
8 // Extra spaces, newlines, etc. for visual alignment with this library code.
9 
10 
11 
12 
13 
14 template<typename T>
15 class vector {
16 
17 
18 
19 
20 
21 
22 
23 
24 legal: // Class invariants (legal).
25     size() >= 0;
26 
27 
28 public:
vector(int count=10)29     explicit vector(int count = 10) :
30         data_(new T[count]),
31         size_(count)
32     {
33         for(int i = 0; i < size_; ++i) data_[i] = T();
34     }
35 
36 
37 
38 
39 
40 
41 
42 
43 
44 
~vector()45     virtual ~vector() { delete[] data_; }
46 
47 
48 
49 
size() const50     int size() const { return size_; }
51 
52 
53 
54 
resize(int count)55     void resize(int count) {
56         T* slice = new T[count];
57         for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i];
58         delete[] data_;
59         data_ = slice;
60         size_ = count;
61     }
62 
63 
64 
65 
66 
67 
68 
69 
70 
71 
operator [](int index)72     T& operator[](int index) { return data_[index]; }
73 
74 
75 
76 
77 
78 
79 
80 
81 
82 
operator [](int index) const83     T& operator[](int index) const { return data_[index]; }
84 
85 
86 
87 
88 axioms: // Preconditions (require) and postconditions (promise) for each func.
89     [int count; require count >= 0; promise size() == count] vector(count);
90     [int count; require count >= 0; promise size() == count] resize(count);
91     [int index; require index >= 0 && index < size()] (*this)[x];       // Op[].
92     [int index; require index >= 0 && index < size()] (*this)[x] const; // Op[].
93 
94 private:
95     T* data_;
96     int size_;
97 };
98 
99 // End.
100 //]
101 
102