#include "find.h"

size_type
find(const value_type* a, size_type n, value_type v)
{
	/*@
	  loop invariant 0 <= i <= n;
	  loop invariant \forall integer k; 0 <= k < i ==> a[k] != v;
	  loop assigns i;
	  loop variant n-i;
	  */
	for (size_type i = 0u; i < n; i++) {
		if (a[i] == v) {
			return i;
		}
	}
	return n;
}

size_type
find2(const value_type* a, size_type n, value_type v)
{
	/*@
	  loop invariant bound:     0 <= i <= n;
	  loop invariant not_found: NoneEqual(a, i, v);
	  loop assigns i;
	  loop variant n-i;
	  */
	for (size_type i = 0u; i < n; i++) {
		if (a[i] == v) {
			return i;
		}
	}
	return n;
}

size_type
find3(const value_type* a, size_type n, value_type v)
{
	/*@
	  loop invariant bound: 0 <= i <= n;
	  loop invariant not_found: Find(a, i, v) == i;
	  loop assigns i;
	  loop variant n-i;
	  */
	for (size_type i = 0u; i < n; i++) {
		if (a[i] == v) {
			//@ assert found: Find(a, n, v) == i;
			return i;
		}
	}
	return n;
}