mirror of
https://github.com/boostorg/contract.git
synced 2026-01-26 18:32:55 +00:00
added all files for release 0.4.0
This commit is contained in:
44
example/meyer97/maxarray.cpp
Executable file
44
example/meyer97/maxarray.cpp
Executable file
@@ -0,0 +1,44 @@
|
||||
|
||||
// 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
|
||||
|
||||
//[meyer97_maxarray
|
||||
// File: maxarray.cpp
|
||||
#include <contract.hpp>
|
||||
#include <boost/detail/lightweight_test.hpp>
|
||||
#include <algorithm>
|
||||
|
||||
CONTRACT_FUNCTION(
|
||||
int (maxarray) ( (int const* const) array, (size_t const&) size )
|
||||
precondition(
|
||||
array, // array allocated
|
||||
size >= 1 // size in range
|
||||
)
|
||||
) {
|
||||
int maxnow = array[0];
|
||||
CONTRACT_LOOP( for(size_t i = 0; i < (size - 1); ++i) ) {
|
||||
// Nested loop (with variant) used to assert enclosing loop invariants.
|
||||
CONTRACT_LOOP( for(size_t j = 0; j < i; ++j) ) {
|
||||
CONTRACT_LOOP_VARIANT( const( i, j ) i - j )
|
||||
CONTRACT_BLOCK_INVARIANT( const( maxnow, array, j )
|
||||
maxnow >= array[j] )
|
||||
}
|
||||
// -2 because starts from 0 (not 1) and already done element at 0.
|
||||
CONTRACT_LOOP_VARIANT( const( size, i ) size - i - 2 )
|
||||
|
||||
maxnow = std::max(maxnow, array[i]);
|
||||
}
|
||||
return maxnow;
|
||||
}
|
||||
|
||||
int main ( void )
|
||||
{
|
||||
int a[] = {1, 5, 3};
|
||||
BOOST_TEST(maxarray(a, 3) == 5);
|
||||
return boost::report_errors();
|
||||
}
|
||||
//]
|
||||
|
||||
Reference in New Issue
Block a user