Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Syntax and Semantics
This lecture will be devoted to a short
introduction to a complex topic. I shall attempt to give the flavour
of the process of program verification, without getting
bogged down in the many details that are involved in actually
constructing rigorous proofs of program properties. I strongly believe
that an understanding of what is involved in the formal verification
of programs is useful in informal reasoning about programs, and the
most important thing to carry away from this lectures is simply a
feeling for what is involved in such formal reasoning. Moreover, the
topic that we shall cover, viz. partial and total correctness of
programs, has strong connections with your everyday programming
experience --- especially programming in groups. You will recognize
familiar concepts like pre- and post-conditions, and loop invariants,
which have origin in the formal treatment of partial correctness
assertions given by pioneers like Floyd and Hoare.
In this lecture, we shall begin by introducing the basic program
verification paradigm and reasoning about straight-line code. We shall
then discuss programs containing if statements and while
loops.
Time and Location
Monday, 13 December, 2004 at 9:00 in room 303.
Reading Material
Primary Reading: Pages 219-227 of
"Abstraction and Specification in Program Development" by Barbara
Liskov and John Guttag, MIT Press, 1986. (If you can get your hands on it!)
Supplementary Optional Reading:
You might interested in looking at the slides for the talk
Verification Engineering: A Future Profession (A. M. Turing
Award Lecture) Sixteenth Annual ACM Symposium on Principles of
Distributed Computing (PODC 1990), San Diego, August, 1997 (abstract,
transparencies.) by Amir Pnueli.
Pages 228-235 and 246-249 of "Abstraction and Specification in
Program Development" by Barbara Liskov and John Guttag, MIT Press,
1986. (If you can get your hands on it!)
Exercises
Prove the validity of the following partial correctness assertion
n>1 {S} sqrt*sqrt <=n<= (sqrt+1)*(sqrt+1)
where S is the following statement in While:
i:=1;
r:= 1;
while r<=n do (i:=i+1;r:=i*i);
sqrt:=i-1
What happens if we replace the pre-condition by n>=0?
Formulate a suitable partial correctness assertion for the
statement below, and prove its validity.
l:=0;
while not(x=1) do (l:=l+1;x:=x-2)
Can you formulate a partial correctness assertion of the form
P {while true do x:=x+1} Q
that does not hold, or is every such assertion valid and provable?
Try to discover appropriate loop invariants yourselves!