// file:          LinearSearcharray.hpp
// description:   Special searchspace using an array and linear search.
//                Sak A16(1), Sak P23, PÜ 31.5(13)(a).
// author:        Karlheinz Hug
// creation date: 2012-06-14
// last update:   2012-07-02

#ifndef LINEAR_SEARCHARRAY_HPP_
#define LINEAR_SEARCHARRAY_HPP_

#include <cassert>

#include "SearcharraySpecial.hpp"

	template <typename T>
	class LinearSearcharray : public SearcharraySpecial<T>
		// Instantiation condition: T is a comparable type.
	{
		protected:
			int index;

			virtual bool is_empty ();

			virtual T item ();

			virtual void init (T x);

			virtual void reduce (T x);

			virtual int position (T x);

			// Verification:
			virtual void loop_invariants (T x);
			virtual bool unequal_before (T x);
	}; // LinearSearcharray

	template <typename T>
	bool LinearSearcharray<T>::is_empty ()
	{
		return index > this->high;
	}

	template <typename T>
	T LinearSearcharray<T>::item ()
	{
		assert(!is_empty()); // precondition
		return this->array[index];
	}

	template <typename T>
	void LinearSearcharray<T>::init (T x)
	{
		index = this->low;
	}

	template <typename T>
	void LinearSearcharray<T>::reduce (T x)
	{
		assert(!is_empty() && item() != x); // precondition
		++index;
	}

	template <typename T>
	int LinearSearcharray<T>::position (T x)
	{
		assert(done(x)); // precondition
		return is_empty() ? this->not_found : index;
	}

	// Verification:

	template <typename T>
	void LinearSearcharray<T>::loop_invariants (T x)
	{
		assert(this->low <= index);
		assert(index <= this->high + 1);
		assert(unequal_before(x));
	}

	template <typename T>
	bool LinearSearcharray<T>::unequal_before (T x)
	{
		assert(index <= this->high + 1); // precondition
		int i = this->low;
		while (i < index && this->array[i] != x)
		{
			++i;
		}
		return i >= index;
	}

#endif // LINEAR_SEARCHARRAY_HPP_