DOC PREVIEW
Berkeley COMPSCI 161 - Defensive Programming

This preview shows page 1-2-3-4 out of 11 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1Defensive ProgrammingDawn [email protected] About Code• Functions make certain assumptions about their arguments– Caller must make sure assumptions are valid– These are often called preconditions• Precondition for f() is an assertion (a logical proposition) that must hold at input to f()– Function f() must behave correctly if its preconditions are met– If any precondition is not met, all bets are off• Caller must call f() such that preconditions true – an obligation on the caller, and callee may freely assume obligation has been met3Simple Precondition Example• int deref(int *p) {return *p;}• Unsafe to dereference a null pointer– Impose precondition that caller of deref() must meet: p ≠ NULL holds at entrance to deref()• If all callers ensure this precondition, it will be safe to call deref()• Can combine assertions using logical connectives (and, or, implication)– Also existentially and universally quantified logical formulas4Another Example• int sum(int *a[], size_t n) {int total = 0, i;for (i=0; i<n; i++)total += *(a[i]);return total;}• Precondition: – Forall j.(0 ≤ j < n) → a[j]≠NULL– If you’re comfortable with formal logic, write your assertions this way for precision• Not necessary to be so formal– Goal is to think explicitly about assumptions and communicate requirements to others5Postconditions• Postcondition for f() is an assertion that holds when f() returns–f() has obligation of ensuring condition is true when it returns– Caller may assume postcondition has been established by f()• Example:• /* Ensures: retval != NULL */void *mymalloc(size_t n) {void *p = malloc(n);if (!p) {perror("Out of memory");exit(1);}return p;}6Process for Writing Function Code• First write down its preconditions and postconditions– Specifies what obligations caller has and what caller is entitled to rely upon• Verify that, no matter how function is called, if precondition is met at function’s entrance, then postcondition is guaranteed to hold upon function’s return – Must prove that this is true for all inputs– Otherwise, you’ve found a bug in either specification (preconditions/postconditions) or implementation (function code)7Proving Precondition→Postcondition• Basic idea:– Write down a precondition and postcondition for every line of code– Apply same sort of reasoning as for function• Requirement:– Each statement’s postcondition must match (imply) precondition of any following statement– At every point between two statements, write down invariant that must be true at that point» Invariant is postcondition for preceding statement, and precondition for next one8Example• Easy to tell if an isolated statement fits its pre- and post-conditions• Valid postcondition for “v=0;”is v=0 (no matter what the precondition is)– Or, if precondition for “v=v+1;”is v≥5, then a valid postcondition is v≥6• If precondition for “v=v+1;”is w≤100, then a valid postcondition is w≤100– Assuming v and w do not alias9Loop Invariant• An assertion that is true at entrance to the loop, on any path through the code– Must be true before every loop iteration» Both a pre- and post-condition for the loop body• Example: Factorial function code– /* Requires: n >= 1 */int fact(int n) {int i, t;i = 1;t = 1;while (i <= n) {t *= i;i++;}return t;}– Prerequisite: input must be at least 1 for correctness– Prove: value of fact() is always positive10Verifying Invariant Correctness• /* Requires: n >= 1Ensures: retval >= 0 */int fact(int n) {int i, t; /* n>=1 */i = 1; /* n>=1 && i==1 */t = 1; /* n>=1 && i==1 && t==1 */while (i <= n) {/* 1<=i && i<=n && t>=1 <-- loop invariant */t *= i; /* 1<=i && i<=n && t>=1 */i++; /* 2<=i && i<=n+1 && t>=1 */} /* i>n && t>=1 */return t;}• Easy if we examine each step:– Function’s precondition implies invariant at function body start– Invariant at end of function body implies function’s postcondition– If each statement matches invariant immediately before and after it, everything’s OK• That leaves the loop invariant…11Verifying the Loop Invariant• Loop invariant: 1<=i && i<=n && t>=1• Prove it is true at start of first loop iteration– Follows from: » n≥1 ∧ i=1 ∧ t=1 → 1≤i≤n ∧ t≥1» if i=1, then certainly i≥1 • Prove that if it holds at start of any loop iteration, then it holds at start of next iteration (if there’s one)– True, since invariant at end of loop body 2≤i≤n+1 ∧ t≥1 and loop termination condition i≤n implies invariant at start of loop body 1≤i≤n ∧ t≥1• Follows by induction on number of iterations that loop invariant is always true on entrance to loop body– Thus, fact() will always make postcondition true, as precondition is established by its caller12Another Example: Recursion• /* Requires: n >= 1 */int fact(int n) {int t;if (n == 1)return 1;t = fact(n-1);t *= n;return t;}• Do you see how to prove that this code always outputs a positive integer?13Analysis• /* Requires: n >= 1Ensures: retval >= 0 */int fact(int n) {int t;if (n == 1)return 1; /* n>=2 */t = fact(n-1); /* t>=0 */t *= n; /* t>=0 */return t;}• Before recursive call to fact(), we know:–n≥1 (by precondition), n≠1 (since if stmt didn’t follow then branch), and n is an integer– Follows that n≥2, or n-1≥1 (means precondition is met when making recursive call)• Can conclude that fact(n-1) return value is positive from postcondition for fact()14Function Post-/Pre-Conditions• Any time we see a function call, we have to verify that its precondition will be met– Then we can conclude its postcondition holds and use this fact in our reasoning• Annotating every function with pre- and post-conditions enables modular reasoning– Can verify function f() by looking only its code and the annotations on every function f() calls» Can ignore code of all other functions and functions called transitively– Makes reasoning about f() an almost purely local activity15Documentation• Pre-/post-conditions serve as useful documentation– To invoke Bob’s code, Alice only has to look at pre- and post-conditions – she doesn’t need to look at or understand his code• Useful way to coordinate activity between multiple programmers:– Each module assigned to one programmer, and pre-/post-conditions are


View Full Document

Berkeley COMPSCI 161 - Defensive Programming

Documents in this Course
Rootkits

Rootkits

11 pages

Load more
Download Defensive Programming
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Defensive Programming and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Defensive Programming 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?