'&$%CSE 303:Concepts and Tools for Software DevelopmentHal PerkinsSpring 2008Lecture 18— Specifications & Error Checking — assertCSE303 Spring 2008, 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”?CSE303 Spring 2008, 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 specificatins (at compile-time and/or run-time) is greatfor finding bugs early and “assigning blame”.CSE303 Spring 2008, 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 cycle or is “balloon” okay?• Postcondition: Sorted (how to specify?) – and a permutation ofthe input (no missing or new elements).And the re’s often m ore 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.CSE303 Spring 2008, 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)CSE303 Spring 2008, 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 postCSE303 Spring 2008, 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.CSE303 Spring 2008, Lecture 18 7'&$%Beyond testingSpecs are useful for more than “things to think about while coding”and te sting and comm ents.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 objec t?CSE303 Spring 2008, 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.CSE303 Spring 2008, Lecture 18 9'&$%assert in JavaIn Java (as of version 1.4):void f(Foo x, Foo y) {assert x != null;assert x != y : "args to f should not be pointer-equal";}• By default, ignored.• At program-start, use command-line options to specify whichpackages’ assertions are enabled.CSE303 Spring 2008, Lecture 18 10'&$%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 because:• 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 debuggingCSE303 Spring 2008, Lecture 18 11'&$%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 m atter, a failure represents aprogramming error (bug). Check this with an assertion.CSE303 Spring 2008, Lecture 18 12'&$%Static checkingA stronger type system or other code-analysis tool might t ake aprogram and examine it for various kinds of errors.• Plusses: earlier detection (“coverage” without running program),faster code• Minus: Potential “false positives” (spec couldn’t ever actually beviolated, but tool thinks so)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.CSE303 Spring 2008, Lecture 18
View Full Document
Unlocking...