// file:          FastLinearSearcharray.hpp
// description:   General searchspace using an array and fast linear search with a sentinel.
//                Sak A16(7)(a), Sak A5, Sak P41, PÜ 31.5(13)(g).
// author:        Karlheinz Hug
// creation date: 2012-06-19
// last update:   2012-07-02

#ifndef FAST_LINEAR_SEARCHARRAY_HPP_
#define FAST_LINEAR_SEARCHARRAY_HPP_

#include <cassert>

#include "SearcharrayGeneral.hpp"

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

			T last_item;

			virtual bool done (T x);

			virtual bool found (T x);

			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);
	}; // FastBinarySearcharray

	template <typename T>
	bool FastLinearSearcharray<T>::done (T x)
	{
		return this->low > this->high || this->array[index] == x;
	}

	template <typename T>
	bool FastLinearSearcharray<T>::found (T x)
	{
		assert(done(x)); // precondition
		if (this->low <= this->high)
		{
			this->array[this->high] = last_item;
			return index < this->high || last_item == x;
		}
		else
		{
			return false;
		}
	}

	template <typename T>
	void FastLinearSearcharray<T>::init (T x)
	{
		index = this->low;
		if (this->low <= this->high)
		{
			last_item               = this->array[this->high];
			this->array[this->high] = x;
		}
	}

	template <typename T>
	void FastLinearSearcharray<T>::reduce (T x)
	{
		assert(!done(x)); // precondition
		++index;
	}

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

	// Verification:

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

	template <typename T>
	bool FastLinearSearcharray<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 // FAST_LINEAR_SEARCHARRAY_HPP_