656/556 2003 1w 16 verification
Assigned work: Ex6.12 (p657) #1(a) & #1(b).
Chapter 4 Verification
  Types of verification
	Proof based
	Semi-automatic
	Property-oriented
	Application Area: Sequential Programs.
	Use Early and use often
  4.1 Background
	Simple facts of life
		Bugs happen and can be dangerous
		They can be found by rigorous and formal proving
		Testing often misses them.
  Handout: Tracing and trace tables.
	A Lite formal method.
	Helps you understand code.
		Handout of a program and a trace
	Uncovers and verifies invariants.
		Handouts
	Exercises
		http://www.csci.csusb.edu/dick/cs656/isqrt0.cpp

  4.2 Framework
	(1) Specification -> Formula.
	(2) Write Program to fit formula.
	(3) Prove that program satisfies formula.
	4.2.1 A Simple Programming Language: While
		Expressionss
		Booleans
		Statements
	Ex 4.1 (p222) #1 #2 #3
	4.2.2 Hoare Triples
		(| \phi |) P (| \psi |)
	     In C++ perhaps:
		//assert( phi );
		P
		//assert( psi );
			The above notation makes it easy to
			convert from assertions to executable debugging.
	4.2.3 Partial vs Total Correctness
	Ex 4.1 #1.
	4.2.4 Program variables and logical variables

  Next 4.3 p231 THE RULES!

Demo: Assertions in C++
   assert but no assertions!
	http://www.csci.csusb.edu/dick/cs656/isqrt0.cpp
   assert and assertions:
	http://www.csci.csusb.edu/dick/cs656/isqrt.cpp
	//pre: precondition on a function call -- must be true before
	//post: postcondition on a function call -- will be true afterwards
	Exercises?

Assigned Work: Exercise 4.1 #2 on page 223 (for in Core).

lab: Print Prof. "Tony" Hoare's seminal paper:
	http://doi.acm.org/10.1145/363235.363259 

Question: how does Hoare's notation differ from the Books?

Question: what kind of  arithmetic do we get with
	unsigned int
and with
	int
in C/C++

 
next: 4.3 calculus
http://www.csci.csusb.edu/dick/cs656/class/17.html