>> [CS656/556 Course Materials]
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
Application Area: Sequential Programs.
Use Early and use often
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.
(1) Specification -> Formula.
(2) Write Program to fit formula.
(3) Prove that program satisfies formula.
4.2.1 A Simple Programming Language: While
Ex 4.1 (p222) #1 #2 #3
4.2.2 Hoare Triples
(| \phi |) P (| \psi |)
In C++ perhaps:
//assert( phi );
//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!
assert and assertions:
//pre: precondition on a function call -- must be true before
//post: postcondition on a function call -- will be true afterwards
Assigned Work: Exercise 4.1 #2 on page 223 (for in Core).
lab: Print Prof. "Tony" Hoare's seminal paper:
Question: how does Hoare's notation differ from the Books?
Question: what kind of arithmetic do we get with
next: 4.3 calculus