// @(#)$Id: LinearSearch.java 1199 2009-02-17 19:42:32Z smshaner $
// Copyright (C) 1998, 1999 Iowa State University
// This file is part of JML
// JML is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2, or (at your option)
// any later version.
// JML is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
// You should have received a copy of the GNU General Public License
// along with JML; see the file COPYING. If not, write to
// the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
package org.jmlspecs.samples.misc;
/** A linear search component, intended to demonstrate verification in
* JML specifications. This class has two abstract methods that
* describe the search, which need to be filled in to instantiate
* it. The formulation of the search and the verification
* is based on Edward Cohen's book
* Programming in the 1990s (Springer-Verlag, 1990).
* @author Gary T. Leavens
*/
public abstract class LinearSearch
{
/** The function that describes what is being sought. */
//@ requires j >= 0;
public abstract /*@ pure @*/ boolean f(int j);
/** The last integer in the search space, this describes the
* domain of f, which goes from 0 to the result.
*/
//@ ensures 0 <= \result;
//@ ensures (\exists int j; 0 <= j && j <= \result; f(j));
public abstract /*@ pure @*/ int limit();
/** Find a solution to the searching problem. */
/*@ public normal_behavior
@ requires (\exists int i; 0 <= i && i <= limit(); f(i));
@ assignable \nothing;
@ ensures \result == (\min int i; 0 <= i && f(i); i);
@*/
public int find() {
int x = 0;
//@ maintaining 0 <= x && (\forall int i; 0 <= i && i < x; !f(i));
//@ decreasing limit() - x;
while (!f(x)) {
/*@ assert 0 <= x && !f(x)
@ && (\forall int i; 0 <= i && i < x; !f(i));
@*/
//@ hence_by (* arithmetic *);
/*@ assert 0 <= (x+1)-1 && !f((x+1)-1)
@ && (\forall int i; 0 <= i && i < (x+1)-1; !f(i));
@*/
x = x + 1;
/*@ assert 0 <= x-1 && !f((int)(x-1))
@ && (\forall int i; 0 <= i && i < x-1; !f(i));
@*/
//@ hence_by (* arithmetic, constant term rule *);
/*@ assert 0 <= x && (\forall int i; i == x-1; !f(i))
@ && (\forall int i; 0 <= i && i < x-1; !f(i));
@*/
//@ hence_by (* joining the range *);
/*@ assert 0 <= x &&
@ (\forall int i; (0 <= i && i < x-1) || i == x-1; !f(i));
@*/
//@ hence_by (* arithmetic *);
//@ assert 0 <= x && (\forall int i; 0 <= i && i < x; !f(i));
}
/*@ assert 0 <= x && f(x)
@ && (\forall int i; 0 <= i && i < x; !f(i));
@*/
//@ hence_by (* definition of \min *);
//@ assert x == (\min int i; 0 <= i && f(i); i);
return x;
}
}