Assume Statements Exercises Key:

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;
}

Asnwer and Explanation: The function above stores the length of array a and creates a new integer array b. Then a for-loop runs for i < a.length, and within the for-loop b[len - 1] = a[i]. This will set the last index of b to the first element in a. After the value of b is set at len-1, len is decremented by 1. This will cause a lot of warnings if we do not specify that both i and (len-1) are in the valid range of zero to a.length. So we need to include this as an assumption anytime we have a loop and need to ensure that we are not going out of bounds. Note that there are better ways of handling loops which we will see in the “Specifying Loops” tutorial, but for now we will handle loops using the assume clause.

//@ ensures \result.length == a.length;
public int[] reverseArray(int[] a) {
	int len = a.length;
	int[] b = new int[len];

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

Learning Objective: The goal of this exercise is to see if the student understands one way that the assume clause can be used at this point in the students’ studies. The tutorial on assume statements goes over this use of assumes well, so it should be easy for the student to determine where the assumption clause should be put to ensure that there are no warnings. This also gives the student a taste of what is to come by using loop invariants which will come later. The questions also requires that the student recall past tutorials.

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;
}

Asnwer and Explanation: Given the code above we are tasked with utilizing the assume clause to find where in the code the error is - since the function is not finding the correct max value in the array. First, let’s break down what the function is doing. The function is first sorting the array using a selection sort, and then sets max = a[a.length-1] - since, if the array is properly sorted in ascending order the max value should be in the last position of the array. Notice the pre and post conditions of the function. The function requires that a != null, typical when using arrays. However, there are two ensures clauses that use a \forall and \exists clause, we haven’t seen how to use these yet as they will come up later in the “JML Expressions” tutorial. Essentially, the first ensures statement checks for the range of 0 to a.length the array should be sorted after the function call. The second ensures statement checks that there exists a max value in the array for the range 0 to a.length.

Now that we understand the code and the pre and postconditions let’s start debugging. First, let’s include our assume statements for the for-loops, since we need to specify that our indices don’t go out of bounds when we iterate through. We will place these where is says “first assume” and “second assume”

//@ 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 = 0; j < a.length; j++) {
			//@ assume 0 <= i < a.length;
			//@ assume 0 <= j < a.length;
			if (a[i] > a[j]) {
				int temp = a[i];
				a[i] = a[j];
				a[j] = temp;
			}
		}
	}
	//third assume	
	//@ assume 0 <= a.length-1 < a.length;
	max = a[a.length-1];
	//fifth assume
	return max;
}

The current code when ran with OpenJML will warn us that the second ensures statement cannot be verified. So we can use the assume clause to check different parts of our code to narrow down where the error might be. First, let’s check the selection sort by using the following assume statement below. We will place this assume statement where it says “third assume.” By placing the assume statement here we are telling OpenJML to assume that our sort works as intended.

//@ 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 = 0; j < a.length; j++) {
			//@ assume 0 <= i < a.length;
			//@ assume 0 <= j < a.length;
			if (a[i] > a[j]) {
				int temp = a[i];
				a[i] = a[j];
				a[j] = temp;
			}
		}
	}
	//@ assume (\forall int i; 0 < i < a.length; a[i-1] <= a[i]);
	//@ assume 0 <= a.length-1 < a.length;
	max = a[a.length-1];
	//firth assume
	return max;
}

When we run this we still get an error that the second ensures statement cannot be verified. So let’s check that our max is being set to the correct value by using another assume statement placed at “fifth assume.”

//@ 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 = 0; j < a.length; j++) {
			//@ assume 0 <= i < a.length;
			//@ assume 0 <= j < a.length;
			if (a[i] > a[j]) {
				int temp = a[i];
				a[i] = a[j];
				a[j] = temp;
			}
		}
	}
	//@ assume (\forall int i; 0 < i < a.length; a[i-1] <= a[i]);
		
	//@ assume 0 <= a.length-1 < a.length;
	max = a[a.length-1];
	//@ assume (\exists int l; 0 < l < a.length; max >= a[l]); 
	return max;
}

After including this second assume statement our function finally verifies - but we have narrowed down that our error must be within the selection sort. You might have already caught it, but in the selection sort we have j = 0, when it needs to be j = i + 1. Something like that might be hard to find in an extensive program, so assume helps us to cut down the time of debugging. If we fix the code we see that the correct max value is found and the function can be verified.

//@ 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++) {
			//@ assume 0 <= i < a.length;
			//@ assume 0 <= j < a.length;
			if (a[i] > a[j]) {
				int temp = a[i];
				a[i] = a[j];
				a[j] = temp;
			}
		}
	}
	//@ assume (\forall int i; 0 < i < a.length; a[i-1] <= a[i]);
		
	//@ assume 0 <= a.length-1 < a.length;
	max = a[a.length-1];
	//@ assume (\exists int l; 0 < l < a.length; max >= a[l]); 
	return max;
}

Learning Objective: The goal of this exercise is to check if the student understands how the assume clause can be used for debugging. In this example the student is told that the code does not work and we want them to go through and use assume to find the error in the code. In doing so the student should see how assume makes debugging more efficient. The student will also see how we still need to use assume right now to make sure that we don’t go out of bounds.

Resources: