CSSE 373 -- Formal Methods in Specification and Design

                               Quiz 11



Name:_________________________________________    Grade:______________


1. What does JML stand for?



2. What are the two things specified by a "BISL"?

	*
	
	
	
	*
	


3. For each of the following comments, indicate (by circling)
   whether or not it is valid JML annotation:

	//@ requires x > 0;                               valid     not valid
	
	
	// @ requires x > 0;                              valid     not valid
	
	
	/*@ requires x > 0;                               valid     not valid
	  @ ensures \result * \result <= x &&
	  @         x < (\result + 1) * (\result + 1);
	  @*/



4. In Design By Contract, what does the engineer specify for each
   function or method?





5. Why are we using JML assertions instead of Java assert statements?






6. What is meant by the "weakest pre-condition" of a statement?








(continued on back)







7. Find the weakest pre-condition:



        //@ assert _______________________________________________________

    x = 10;
        //@ assert x + y == 20;





8. Find the weakest pre-condition:



        //@ assert _______________________________________________________




    i = i + 1;
        //@ assert 0 <= i && i <= n && i < j;





9. Fill in the weakest pre-conditions:





        //@ assert _______________________________________________________




    temp = i;

        //@ assert _______________________________________________________




    i = j;

        //@ assert _______________________________________________________




    j = temp;
        //@ assert i == 10 && j == 20;