[Index] || [Contents] || [Grades] Wed Mar 12 07:12:05 PST 2003

656/556 2003 1w 18 Total Correctness admin: Planning presentations Date and Time of Final Deadlines! All work in before the final. Some previous work needs to be redone. Assigned work due in: Exercises 4.3 page 242 #1c Wind up class/17 http://www.csci.csusb.edu/dick/cs656/class/17.html Section 4.4 Total correctness Total correctness proves that a program both terminates in a finite number of steps AND produces the correct postconditions. Usually termination is comparatively trivial and a part of the analysis of the algorithms --- taught in other classes. However in some case termination is very hard to show. There is no algorithm that will tell you whether a given program terminates or not (standard theory of computation). There exist algorithms where termination can not be proved and non-termination can not be proved! There is a very simple algorithm and nobody knows (for certain) if it always terminates or if some data will take it into an infinite loop. The book presents a technique borrowed from Dijkstra of introducing both an invariant and a variant expression into each loop. Invariant: if P is true at the start the it is true afterward. Variant: if E has value E0 at the start then it has a value < E0 afterward. Only one rule is modified. In pace of the While rule we have P and E>=0 { while (B) {C} } P and not B is true if P and B and 0<=E=E0 {C} P and 0 <= E < E0. Conclusion: It is better to design programs so that termination and correctness are easier to verify, than it is to invent programs and then try to prove them totally correct. Assigned work: Exercises 4.6 page 250-251 While loops #1 Hint: the invariant is x=y+a. lab: Review of Course: Basic logic, OBDDs, CTL, and Verification Revisit all the class pages: http://www.csci.csusb.edu/dick/cs656/class/ next Plan for Presentations in classes 19 and 20 http://www.csci.csusb.edu/dick/cs656/class/19.html