boost/contract
2
0
Fork 0
mirror of https://github.com/boostorg/contract.git synced 2026-02-26 16:42:19 +00:00
Code Issues Projects Releases Wiki Activity

tested access on msvc, gcc, clang, and wave

Browse Source
This commit is contained in:
Lorenzo Caminiti
2014-10-19 23:44:29 -07:00
parent 29fb97573b
commit 570b283bf2
135 changed files with 36 additions and 9323 deletions
Download Patch File Download Diff File Expand all files Collapse all files

144
example/cline90/vstack.cpp
View File

@@ -1,144 +0,0 @@
// Copyright (C) 2008-2012 Lorenzo Caminiti
// Distributed under the Boost Software License, Version 1.0
// (see accompanying file LICENSE_1_0.txt or a copy at
// http://www.boost.org/LICENSE_1_0.txt)
// Home at http://sourceforge.net/projects/contractpp
//[cline90_vstack
// File: vstack.cpp
#include "vector.hpp"
#include <contract.hpp>
#include <boost/detail/lightweight_test.hpp>
CONTRACT_CLASS( // Stack Abstract Data Type (ADT).
template( typename T )
class (stack_adt)
) {
// NOTE: Incomplete set of assertions addressing only empty/full issues.
CONTRACT_CLASS_INVARIANT_TPL( void ) // no invariants
CONTRACT_CONSTRUCTOR_TPL(
public (stack_adt) ( void )
// postcondition:
// empty (cannot be checked because empty's postcondition uses
// length which is pure virtual during construction)
) {}
CONTRACT_DESTRUCTOR_TPL(
public (~stack_adt) ( void )
) {}
CONTRACT_FUNCTION_TPL(
public bool (full) ( void ) const
postcondition(
auto result = return,
result == (length() == capacity())
)
) {
return length() == capacity();
}
CONTRACT_FUNCTION_TPL(
public bool (empty) ( void ) const
postcondition( auto result = return, result == (length() == 0) )
) {
return length() == 0;
}
CONTRACT_FUNCTION_TPL(
public virtual int (length) ( void ) const
postcondition( auto result = return, result >= 0 )
) = 0;
CONTRACT_FUNCTION_TPL(
public virtual int (capacity) ( void ) const
postcondition( auto result = return, result >= 0 )
) = 0;
CONTRACT_FUNCTION_TPL(
public virtual void (push) ( (T) value )
precondition( not full() )
postcondition( not empty() )
) = 0; // Contract for pure virtual function.
CONTRACT_FUNCTION_TPL(
public virtual (T) (pop) ( void )
precondition( not empty() )
postcondition( not full() )
) = 0;
CONTRACT_FUNCTION_TPL(
public virtual void (clear) ( void )
postcondition( empty() )
) = 0;
};
CONTRACT_CLASS( // Vector-based stack.
template( typename T )
class (vstack) extends( public stack_adt<T> )
) {
CONTRACT_CLASS_INVARIANT_TPL(
length() >= 0,
length() < capacity()
)
CONTRACT_CONSTRUCTOR_TPL(
public explicit (vstack) ( int count, default 10 )
precondition( count >= 0 )
postcondition( length() == 0, capacity() == count )
initialize( vect_(count), length_(0) ) // OK, after preconditions.
) {}
CONTRACT_DESTRUCTOR_TPL(
public virtual (~vstack) ( void )
) {}
// NOTE: All following inherit contracts from `stack_adt`.
CONTRACT_FUNCTION_TPL(
public int (length) ( void ) const override final
) {
return length_;
}
CONTRACT_FUNCTION_TPL(
public int (capacity) ( void ) const
) {
return vect_.size();
}
CONTRACT_FUNCTION_TPL(
public void (push) ( (T) value ) override final
) {
vect_[length_++] = value;
}
CONTRACT_FUNCTION_TPL(
public (T) (pop) ( void ) override final
) {
return vect_[--length_];
}
CONTRACT_FUNCTION_TPL(
public void (clear) ( void ) override final
) {
length_ = 0;
}
private: vector<T> vect_;
private: int length_;
};
int main ( void )
{
vstack<int> s(3);
BOOST_TEST(s.capacity() == 3);
s.push(123);
BOOST_TEST(s.length() == 1);
BOOST_TEST(s.pop() == 123);
return boost::report_errors();
}
//]