org.jmlspecs.samples.misc
Class Proof

java.lang.Object
  org.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.

Proof

public Proof()

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.