656/556 2003 1w 17 veri calc
Assigned Work: Exercise 4.1 #2 on page 223 (for in Core).

4.3 Calculus of program verification
4.3.1 Proof Rules
  Fig4.1
	http://www.csci.csusb.edu/dick/cs656/class/17rules.html#PartialCorrectness
  Assignment Rule
  Examples 4.7
  If-Statements
  While Statements
	Each loop needs you to create an invariant property.
  Implied Rule
4.3.2 Proof Tableaux
  Fig 4.2
  Better --- embed invariants in the code:
     Assignement
 	//assert( P[E/x] )
 	x = E
	//assert( P )
     While loop
	while(B)
	//inv: P
	{ //assert( (B)  && (P) );
		...
	 //assert( P);
	}//assert( !(B) && (P) );

Exercises 4.3 page 242 Assignments #1 #2 #3

Exercises 4.4 page 244 Ifs #1 #2

Exercises 4.5 page 245 Implications #1 #2 #3

Exercises 4.6 page 250-252 While loops #1 #2 #3 #4 #5 #6 #7

4.3.3 Case Study:  Minimal sum section

Exercise 4.7 page 254 #1 #2 #3

Exercise 4.8 page 257  #1 #2

More Demo/exercises
	http://www.csci.csusb.edu/dick/cs656/enigma.cpp

Assigned Work:
Exercises 4.3 page 242  #1c

lab:
	http://www.cis.ksu.edu/~huth/lics/tutor/chap4/questions.html

Next: Total correctness
http://www.csci.csusb.edu/dick/cs656/class/18.html