[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS656/556 Course Materials] >> class/16
[Index] || [Contents] || [Grades] Mon Mar 3 14:43:02 PST 2003
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