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