Method Specifications Exercises:

Method Specifications Tutorial

Question 1

Given the program below, correct the order of the specifications for easier readability.

public class Pet {
	
	public String species;
	public String name;
	public int yearsOld;
	public double weight;
	public boolean vaccinated;
	/**total number of pet's owned by the owner**/
	//@ spec_public
	private static int numPets = 0; 
	
	//@ public normal_behavior
  	//@ 	ensures numPets == \old(numPets) + 1;
  	//@ 	assigns numPets;
  	//@	ensures this.species == species;
	//@	requires species.length() > 0;
  	//@ 	ensures this.name == name;
	//@ 	requires name.length() > 0;
  	//@ 	ensures this.yearsOld == yearsOld;
	//@ 	ensures this.weight == weight;
	//@ 	requires 0 <= yearsOld < 100;
  	//@ 	requires weight > 0;
	//@ 	requires !Double.isNaN(weight);
	//@ 	ensures this.vaccinated == vaccinated;
	public Pet(String species, String name, int yearsOld, double weight, boolean vaccinated) {
		this.species = species;
		this.name = name;
		this.yearsOld = yearsOld;
		this.weight = weight;
		this.vaccinated = vaccinated;
		
		//@ assume numPets + 1 < Integer.MAX_VALUE;
		numPets++;
	}
}

Learning Objectives:

  • Understand the standard for writing specifications in JML
  • Understand the importance of ordering specifications
  • Understand that the order of preconditions do matter

Answer Key

All exercises