Aside from explicitly stating the invariant, will it also be necessary to explicitly state the preassertion/postassertion?Absolutely essential. I understand ``preassertion/postassertion'' above to refer to the procedure as a whole. The preassertion indicates the assumptions about the input (which may include some bounds as well as the array) that the program requires. The postassertion must say enough to conclude that the result is correct, given that the program halts and that it doesn't change the wrong things (in this case, the wrong things are the entries in the array, and possibly some other variables that you decide shouldn't be changed). In Bentley, it is hard to distinguish between what is are the assertions and the invariant.Yep. That's your problem. For a real careful layout of this style of reasoning, look at the short paper by Nadathur (PostScript format) that I reference in the lecture notes. How will points be distributed for the assignment, in other words, what necessary elements need to be there aside from a working, correct program?In this class, a ``working'' program will never count for much. This is not a programming class. The purpose of all programs in this class is to generate insight about programming language structure, not to produce a particular output. Here's my grading scheme from last year. I might refine it a bit this year, but probably not. I alotted 25 points for the assignment: 5 for each of the following points:I didn't allocate points explicitly for preassertion and postassertion, but your presentation will not be very convincing without them, and you'll lose in some category or other. Mike O'D. |
to: