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

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] protected  int	min           A variable to keep track of the minimum.
[spec_public] private  int	res           The index where the element occurs for exercise 2.

 

Constructor Summary

Proof()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

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.

Specifications: spec_public

res

private int res

The index where the element occurs for exercise 2.

Specifications: spec_public

Proof

public Proof()

find_min

public void find_min(int[] a)

Exercise 1: find the minimum element in an array.

Specifications:

public normal_behavior
requires a != null&&a.length >= 1;
assignable min;
ensures ( \forall int i; 0 <= i&&i < a.length; this.min <= a[i])&&( \exists int i; 0 <= i&&i < a.length; this.min == a[i]);

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.

Specifications:

public normal_behavior
requires a != null&&( \exists int i; 0 <= i&&i < a.length; a[i] == x);
assignable res;
ensures 0 <= this.res&&this.res < a.length&&a[this.res] == x;