Function Specifications: Preconditions, Postconditions & Assertions

Download Presenatation
preconditions postconditions assertions n.w
1 / 23
Embed
Share

Discover the significance of preconditions, postconditions, and assertions in defining function specifications. Learn how these conditions ensure correct function behavior and facilitate communication among developers.

  • Function Specification
  • Preconditions
  • Postconditions
  • Assertions
  • Programming

Uploaded on | 5 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.

E N D

Presentation Transcript


  1. Preconditions, Postconditions & Assertions

  2. Function Specification Often want to communicate what a function does without indicating how it works: The specification of a function can be defined by its pre-conditions and post-conditions. pre-condition: a condition that must be true of the parameters of a function prior to running the function post-condition: a condition that is true after running the function

  3. Precondition A precondition must be true when the function is called Constraint on the client (the one calling the function) Precondition is assumed to be true by the function's implementor

  4. Postcondition Postcondition is guaranteed to be true after the function's execution terminates (IF the preconditions were satisfied when the function was called) Constraint on implementor Assumed true by client

  5. Examples Write precondition and postcondition for: pop() function for a stack Recall the prototype for pop(): int pop(Stack s);// remove & return top stack element

  6. Examples What are reasonable pre- and postconditions for the binarySearch function? int binarySearch(int arr[], int N, int key) { int mid; int min = 0; int max = N-1; while(min <= max) { mid = (min + max)/2; if(key == arr[mid]) return mid; else if(key < arr[mid]) max = mid 1; else min = mid + 1; } return -1; }

  7. Stack ADT Stack.h: #include<stdbool.h> typedef struct stackType *Stack; Stack create(); void destroy(Stack s); bool isEmpty(Stack s); // return true if stack is empty, false otherwise bool isFull(Stack s); // return true if stack is full, false otherwise void push(Stack s, int n); // add n to top of stack int pop(Stack s); // remove and return top stack element // create new empty stack // remove stack and all its elements

  8. Example // Precondition: x >= 0 // Postcondition: Returns the square root of x double computeSqrt(double x) { ... } Precondition x >= 0 must be true when function is called. Otherwise, result of function call unpredictable. Which function calls meet the precondition? computeSqrt(-49); computeSqrt(0); computeSqrt(3.9);

  9. Example // Precondition: x >= 0 // Postcondition: Returns the square root of x double computeSqrt(double x) { ... } Postcondition indicates the result of the function call the function returns the square root of x

  10. Example // Precondition: letter is an uppercase or lowercase // letter //Postcondition: Returns true if letter is a vowel, and // returns false otherwise bool isVowel(char letter) { ... } What will be returned by these calls? isVowel('a'); isVowel('B'); isVowel('$');

  11. Exercise Consider our Stack ADT. Write down preconditions and postconditions for: isEmpty function top function

  12. Satisfy the Preconditions If you are calling a function, you must ensure that the precondition is true when the function is called! Otherwise, no guarantee about what the function does.

  13. Postcondition Pre- and post-conditions are a contract on the function's behavior: if precondition true when you call function, then postcondition is true when function returns "Design by contract"

  14. Checking Preconditions As the function implementor, you aren't responsible for your function's behavior if the precondition is not satisfied when it's called. Who is? But: when you write a function, try to detect a precondition violation If a precondition is violated, terminate execution

  15. Why Use Pre/Post Conditions? Specify what a function accomplishes without describing how it works Makes it easier for you to change your implementation later: Given the same pre- and post-conditions, clients should be unaffected by the implementation change

  16. Assertions and Program Logic "As soon as we started programming, we found to our surprise that it wasn't as easy to get programs right as we had thought. Debugging had to be discovered. I can remember the exact instant when I realized that a large part of my life from then on was going to be spent in finding mistakes in my own programs." --Maurice Wilkes

  17. Question What is the output of this function? void mystery(bool b) { printf("%d ", b); b = (b == false); printf("%d", b); } A. no output syntax error B. no output runtime error C. not possible to determine output D. always outputs 0 1 OR 1 0 E. always outputs 1 1 OR 0 0

  18. Assertions Assertion: A declarative statement that is either true or false Examples: 2 + 2 equals 4 x > 45 It is raining. It rained in Austin, TX, on October 30, 1999. UT beat San Jose State this year. Not assertions How old are you? Take me to H.E.B.

  19. Assertions The value of assertions (true or false) sometimes dependent on context. Which of these depend on context? 2+2 = 5 x > 45 The Chicago Cubs played in the world series last year It is raining.

  20. Assertions Assertions that depend on context can be evaluated when context is provided. When x is 50, x > 45 The Chicago Cubs played in the world series in 2016.

  21. Assertions and Program Logic Assertions help us reason about our programs Help with debugging

  22. Assertions in C You can use the C library macro assert(): void assert(int expression); if expression is true, assert() does nothing if expression is false, assert() displays an error message Check that precondition is true with an assertion: #include<assert.h> // Precondition: x >= 0 // Postcondition: Returns the square root of x double computeSqrt(double x) { assert(x >= 0); ... } If the assertion is false, the program will halt and print an error message.

  23. Assertion Example: Checking User Input #include<assert.h> #include<stdio.h> int main() { int num; printf("Enter a positive integer: "); scanf("%d", &num); assert(num > 0); printf("Yay, a positive int!\n"); } Sample Run: Enter a positive integer: -2 Assertion failed: (num > 0), function main, file assertEx.c, line 8.

Related


More Related Content