CMPS 253 Midterm, Fall 2010

CMPS 253 Software Engineering — Fall 2010–11 Section 1 MIDTERM EXAM 50 minutes December 8, 2010 Please draw a horizontal line across the page between the answers to each question You may refer to the following during the exam: • the course textbook • the course lecture notes • your homework solutions • any notes that you have taken in class You may not refer to any other materials. Good luck! 1. (40 points) You will receive no credit if you do not show intermediate assertions. (a, 10 points) Find a nontrivial (i.e., not identical to false) precondition P so that the following is valid, where x, y are integer variables. Show all intermediate assersions. {P} y = x; x = y; {x + y = 0} (b, 10 points) Find a nontrivial (i.e., not identical to true) postcondition Q so that the following is valid, where x, y are integer variables. Show all intermediate assersions. {x + y = 0} x = −x; y = x; {Q} (c, 20 points) Find a nontrivial (i.e., not identical to false) precondition P so that the following is valid, where x, y, z are integer variables. Show all intermediate assersions. {P} if (even(x)) x = x/2; y = y ∗ 2; else z = z + y; x = x − 1; endif {z + x ∗ y = C} 1 2. (60 points) Write an instance method union for the IntSet data abstraction that satisfies the following specification (where U denotes the set union operator): public void union(IntSet s) //REQUIRES: s != null //EFFECTS: AF(els,top)_post = AF(els,top) U AF(s.els, s.top) //MODIFIES: els, top Your method is to be implemented within the IntSetNoDupSort implementation. You earn the 60 points for this question as follows: (a, 20 points) Write code that is correct. (b, 20 points) Annotate the code with assertions, and use these to show that the code is correct, i.e., that the postcondition (EFFECTS clause) holds upon termination provided that the precondition s ̸= null holds initiallly. (c, 20 points) Show that your implementation runs in time O(top + s.top). 2