JML

org.jmlspecs.samples.misc
Class Proof

java.lang.Object
  extended byorg.jmlspecs.samples.misc.Proof

public class Proof
extends Object

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

Field Summary
protected  int min
          A variable to keep track of the minimum.
private  int res
          The index where the element occurs for exercise 2.
 
Constructor Summary
Proof()
           
 
Method Summary
 void find(int[] a, int x)
          Exercise 2: find the index of an integer in an array.
 void find_min(int[] a)
          Exercise 1: find the minimum element in an array.
 int getRes()
          Return the value of res
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

min

protected int min
A variable to keep track of the minimum.


res

private int res
The index where the element occurs for exercise 2.

Constructor Detail

Proof

public Proof()
Method Detail

find_min

public void find_min(int[] a)
Exercise 1: find the minimum element in an array.


getRes

public int getRes()
Return the value of res


find

public void find(int[] a,
                 int x)
Exercise 2: find the index of an integer in an array.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.