JML Tutorial - Exercises - Assume Statements

Assume Statements Exercises:

Assume Statements Tutorial

Question 1

Given the function below, determine the specifications needed to verify the function, as well as including the assume statements where indicated.

public int[] reverseArray(int[] a) {
	int len = a.length;
	int[] b = new int[len];

	for (int i = 0; i < a.length; i++) {
		//first assume 
		//second assume
		b[len - 1] = a[i];
		len--;			
	}
	//@ assert b.length == a.length;
	return b;
}

Learning Objectives:

Understand how assume can be used for loops
Understand there are better ways of dealing with loops

Question 2

The following code has an error with finding the max value in an array. Determine how assume can be used to find where in the code the error occurs.

//@ requires a != null;
//@ ensures (\forall int k; 0 < k < a.length; a[k-1] <= a[k]);
//@ ensures (\exists int k; 0 < k < a.length; \result >= a[k]);
public int sortFindMax(int[] a) {
	int max;

	for (int i = 0; i < a.length-1; i++) {
		for (int j = i+1; j < a.length; j++) {
			//first assume
			//second assume
			if (a[i] > a[j]) {
				int temp = a[i];
				a[i] = a[j];
				a[j] = temp;
			}
		}
	}
	//third assume 
	//fourth assume
	max = a[a.length-1];
	//fifth assume
	return max;
}