'&$%CSE 303:Concepts and Tools for Software DevelopmentHal PerkinsWinter 2009Lecture 18— Specifications & Error Checking — assertCSE 303 Winter 2009, Lecture 18 1'&$%Where are We• Talked about testing, but not what (partially) correct was• What does it mean to say a program is “correct”?• How do we talk about what a program should “do”?• What do we do w hen it “doesn’t”?CSE 303 Winter 2009, Lecture 18 2'&$%Specifying Code?We m ade a big assumption, that we know what the code is supposedto do!Oftentimes, a complete specification is at least as difficult as writingthe code. But:• It’s still worth thinking about.• Partial specifications are better than none.• Checking specifications (at compile-time and/or run-time) is greatfor finding bugs early and “assigning blame”.CSE 303 Winter 2009, Lecture 18 3'&$%Full SpecificationOften tractable for very simple stuff: “Take an int x and return 0 iffthere exists ints y and z such that y ∗ z == x (where x, y, z > 0and y, z < x).”What about sorting a doubly-linked list?• Precondition: Can input be NULL? Can any prev and next fieldsbe NULL? Must it be a cyc le or is “balloon” okay?• Postcondition: Sorted (how to spec ify?) – and a permutation ofthe input (no missing or new elements).And there’s often more than “pre” and “post” – time/space overhead,other effects (such as printing), things that may happen in parallel.Specs should guide programming and testing! Should be declarative(“what” not “how”) to dec ouple implementation and use.CSE 303 Winter 2009, Lecture 18 4'&$%Pre/post and invariantPre- and post-conditions apply to any statement, not just functions• What is assumed before and guaranteed afterBecause a loop “calls itself” its body’s post-condition better imply theloop’s precondition.• A loop invariantExample: find max (next slide)CSE 303 Winter 2009, Lecture 18 5'&$%Pre/post and invariant// pre: arr has length len; len >= 1int max = arr[0];int i=1;while(i<len) {if(arr[i] > max)max = arr[i];++i;}// post: max >= all arr elementsloop-invariant: For all j<i, max>=arr[j].• to show it holds after the loop body, must assume it holds beforeloop body• loop-invariant plus !(i<len) after body, enough to show postCSE 303 Winter 2009, Lecture 18 6'&$%Partial SpecificationsThe difficulty of full specs need not mean abandon all hope.Useful partial specs:• Can args be NULL?• Can args alias?• Are stack pointers allowed? Dangling pointers?• Are cycles in data structures allowed?• What is the minimum/maximum length of an array?• ...Guides callers, callees, and testers.CSE 303 Winter 2009, Lecture 18 7'&$%Beyond testingSpecs are useful for more than “things to think about while coding”and testing and comments.Sometimes you can check them dynamically, e.g., with assertions (allexamples true for C and Java)• Easy: argument not NULL• Harder but doable: list not cyclic• Impossible: Does the caller have other pointers to this object?CSE 303 Winter 2009, Lecture 18 8'&$%assert in CIn C:#include <assert.h>void f(int *x, int*y) {assert(x!=NULL);assert(x!=y);...}• A macro; ignore argument if NDEBUG defined at time of #include,else evaluate and if zero exit with file/line number.• Watch Out! Be sure that none of the code in an assert has sideeffects that alter the program’s behavior. Otherwise you getdifferent results when assertions are enabled vs. when they are not.CSE 303 Winter 2009, Lecture 18 9'&$%assert styleMany oversimply say “always” check everything you can. But:• Often not on “private” functions (caller already checked)• Unnecessary if chec ked statically“Disabled” in released code bec ause:• executing them takes time• failures are not fixable by users anyway• assertions themselves could have bugs/vulnerabilitiesOthers say:• Should leave enabled; corrupting data on real runs is worse thanwhen debuggingCSE 303 Winter 2009, Lecture 18 10'&$%asserts and error checkingSuppose a condition should be true at a given point in the program,but it’s not. What do we do?One widely used strategy is:• If the condition involves preconditions for using a public interface(x ≥ 0, list not full, . . . ), treat a failure as an error and throw anexception or te rminate with an error code.– Don’t trust client code you don’t control!• If the condition is an internal matter, a failure represents aprogramming error (bug). Check this with an assertion.CSE 303 Winter 2009, Lecture 18 11'&$%Static checkingA stronger type system or other c ode-analysis tool might take aprogram and examine it for various kinds of e rrors.• Plusses: earlier detection (“coverage” without running program),faster code• Minus: Potential “false positives” (spec couldn’t ever actually beviolated, but tool can’t prove that)Deep CSE322 fact: Every code-analysis tool proving a non-trivial facthas either false positives (unwarranted warning) or false negatives(missed bug) or both.Deep real-world fact: That doesn’t make them unuseful.CSE 303 Winter 2009, Lecture 18
View Full Document
Unlocking...