CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 12



Name:_________________________________________    Grade:______________



1. Find P, the weakest pre-condition for the following program fragment.
   Show your work.
   

	P is _______________________


		//@ assert P;
	
	if (x > y) {
	
	
	
	
	
		m = x;
	
	
	
	} else {
	
	
	
	
	
		m = y;
	
	
	
	}
		//@ assert m >= x && m >= y;











(continued on back)















2. Find P, the weakest pre-condition for the following program fragment.
   Show your work. (Note: 365 * 2 == 730)
   

	P is _______________________

		//@ assert P;
	
	
	
	
	
	
		
	
	
	
	
	
	
	if (d >= 365) {
	
	
	
	
	
	
	
		y = 1;
	
	
	
		d = d - 365;
	
	
	
	} else {
	
	
	
	
	
		y = 0;
	
	
	
	}
		//@ assert 0 <= d && d < 365;




3.  Is a loop invariant true right after the loop finishes, that is,
    when the loop condition becomes false?