// @(#)$Id: Proof.java-refined,v 1.1 2003/05/23 22:31:06 leavens Exp $

// Copyright (C) 2000 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 class that demonstrates Floyd-Hoare-style proofs using JML
 * notation.  This was originally used as an exercise for a class at
 * the University of Iowa.
 * @author Gary T. Leavens */
public class Proof {

    protected /*@ spec_public @*/ int min = Integer.MAX_VALUE;

    /** Exercise 1: implement and prove correct a method that
     *  satisfies the following specification. */
    /*@ public normal_behavior
      @   requires a != null;
      @   assignable min;
      @   ensures (\forall int i; 0 <= i && i < a.length; min <= a[i])
      @      && (\exists int i; 0 <= i && i < a.length; min == a[i]);
      @*/
    public void find_min (int a[]);

    private /*@ spec_public @*/ int res = 0;

    /** Exercise 2: implement and prove correct a method that
     *  satisfies the following specification. */
    /*@ public normal_behavior
      @   requires a != null
      @      && (\exists int i; 0 <= i && i < a.length; a[i] == x);
      @   assignable res;  // not included but necessary!
      @   ensures 0 <= res && res < a.length && a[res] == x;
      @*/
    public void find(int a[], int x);

}