From e62354d3f6672e4cd1ce83ee5f457e2c63986ceb Mon Sep 17 00:00:00 2001 From: SpecBot Date: Tue, 27 Jan 2026 21:00:56 +0000 Subject: [PATCH] Add formal specifications to vector class - Add check_invariant() method with core class invariants - Add invariant checks to all constructors and destructor - Add invariant preservation checks to mutating methods - Add pre-condition documentation to critical operations - Add post-condition checks after state modifications Class invariants added: - size() <= capacity() (fundamental size/capacity relationship) - m_data == nullptr implies size() == 0 && capacity() == 0 - m_data != nullptr implies capacity() > 0 Improves runtime error detection and documents class contracts. --- src/util/vector.h | 51 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 41 insertions(+), 10 deletions(-) diff --git a/src/util/vector.h b/src/util/vector.h index ad2802e92..4d7209a66 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -54,6 +54,16 @@ class vector { #define CAPACITY_IDX -2 T * m_data = nullptr; + // Class invariant checking + void check_invariant() const { + // Fundamental invariant: size never exceeds capacity + SASSERT(size() <= capacity()); + // Null data implies zero size and capacity + SASSERT(m_data != nullptr || (size() == 0 && capacity() == 0)); + // Non-null data implies positive capacity + SASSERT(m_data == nullptr || capacity() > 0); + } + void destroy_elements() { std::destroy_n(m_data, size()); } @@ -78,7 +88,7 @@ class vector { } else { static_assert(std::is_nothrow_move_constructible::value); - SASSERT(capacity() > 0); + SASSERT(capacity() > 0); // Pre-condition: existing capacity must be positive SZ old_capacity = reinterpret_cast(m_data)[CAPACITY_IDX]; SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; SZ new_capacity = (3 * old_capacity + 1) >> 1; @@ -133,11 +143,13 @@ public: vector(SZ s) { init(s); + check_invariant(); } void init(SZ s) { SASSERT(m_data == nullptr); if (s == 0) { + check_invariant(); return; } SZ * mem = reinterpret_cast(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2)); @@ -152,10 +164,12 @@ public: for (; it != e; ++it) { new (it) T(); } + check_invariant(); } vector(SZ s, T const & elem) { resize(s, elem); + check_invariant(); } vector(vector const & source) { @@ -163,24 +177,30 @@ public: copy_core(source); } SASSERT(size() == source.size()); + check_invariant(); } vector(vector&& other) noexcept { std::swap(m_data, other.m_data); + check_invariant(); } vector(SZ s, T const * data) { + SASSERT(s == 0 || data != nullptr); // Pre-condition: non-null data for non-zero size for (SZ i = 0; i < s; ++i) { push_back(data[i]); } + check_invariant(); } vector(std::initializer_list const& l) { for (auto const& t : l) - push_back(t); + push_back(t); + check_invariant(); } - ~vector() { + ~vector() { + check_invariant(); destroy(); } @@ -217,6 +237,8 @@ public: else { m_data = nullptr; } + check_invariant(); // Post-condition: invariant established + SASSERT(size() == source.size()); // Post-condition: size matches source return *this; } @@ -227,6 +249,7 @@ public: destroy(); m_data = nullptr; std::swap(m_data, source.m_data); + check_invariant(); // Post-condition: invariant established return *this; } @@ -282,6 +305,7 @@ public: } reinterpret_cast(m_data)[SIZE_IDX] = 0; } + check_invariant(); // Post-condition: invariant holds after reset } void clear() { reset(); } @@ -401,11 +425,12 @@ public: } void pop_back() { - SASSERT(!empty()); + SASSERT(!empty()); // Pre-condition: vector must not be empty if (CallDestructors) { back().~T(); } - reinterpret_cast(m_data)[SIZE_IDX]--; + reinterpret_cast(m_data)[SIZE_IDX]--; + check_invariant(); // Post-condition: invariant preserved } vector& push_back(T const & elem) { @@ -414,6 +439,7 @@ public: } new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(elem); reinterpret_cast(m_data)[SIZE_IDX]++; + check_invariant(); return *this; } @@ -430,6 +456,7 @@ public: } new (m_data + reinterpret_cast(m_data)[SIZE_IDX]) T(std::move(elem)); reinterpret_cast(m_data)[SIZE_IDX]++; + check_invariant(); return *this; } @@ -438,7 +465,7 @@ public: } void erase(iterator pos) { - SASSERT(pos >= begin() && pos < end()); + SASSERT(pos >= begin() && pos < end()); // Pre-condition: valid iterator iterator prev = pos; ++pos; iterator e = end(); @@ -446,6 +473,7 @@ public: *prev = std::move(*pos); } pop_back(); + check_invariant(); // Post-condition: invariant preserved } void erase(T const & elem) { @@ -471,7 +499,7 @@ public: void shrink(SZ s) { if (m_data) { - SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); + SASSERT(s <= reinterpret_cast(m_data)[SIZE_IDX]); // Pre-condition: can only shrink to smaller size if (CallDestructors) { iterator it = m_data + s; iterator e = end(); @@ -482,8 +510,9 @@ public: reinterpret_cast(m_data)[SIZE_IDX] = s; } else { - SASSERT(s == 0); + SASSERT(s == 0); // Pre-condition: null data implies shrinking to zero } + check_invariant(); // Post-condition: invariant preserved } template @@ -493,13 +522,14 @@ public: while (s > capacity()) { expand_vector(); } - SASSERT(m_data != 0); + SASSERT(m_data != 0); // Post-condition: data allocated after expansion reinterpret_cast(m_data)[SIZE_IDX] = s; iterator it = m_data + sz; iterator end = m_data + s; for (; it != end; ++it) { new (it) T(std::forward(args)); } + check_invariant(); // Post-condition: invariant holds after resize } void resize(SZ s) { @@ -508,13 +538,14 @@ public: while (s > capacity()) { expand_vector(); } - SASSERT(m_data != 0); + SASSERT(m_data != 0); // Post-condition: data allocated after expansion reinterpret_cast(m_data)[SIZE_IDX] = s; iterator it = m_data + sz; iterator end = m_data + s; for (; it != end; ++it) { new (it) T(); } + check_invariant(); // Post-condition: invariant holds after resize } void append(vector const & other) {