[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/17
[Index] || [Contents] || [Grades] Wed Mar 5 13:07:46 PST 2003
```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
```