Final Review
General information
- Read all notes and given assignments
First part (questions on materials up to and including those in Midterm)
- Review the Midterm review
- Review the Midterm itself, and pay close attention to things that you did wrong (e.g., worst case DD).
Second part (questions on materials learned after Midter)
- Floyd Hoare logic
- Know Hoare logic
- Know how to do logical reasoning (e.g., simplify basic algebra, know how to check if something simplified to
True
orFalse
, etc) - Know how to compute weakest preconditions for a given program wrt to a given post condition
Q
- Know how to form the verification condition from obtained
wp
and the given preconditionP
and show/prove that the verification condition is correct (i.e., show the program is correct wrt to givenP
andQ
) - Know loop invariants
- Able to show when a candidated (guessed) invariant is really a loop invariant or not
- Able to show when a candidate invariant (that is indeed a loop invariant) is not strong enough to show the Hoare triple
- Able to show when a candidate invariant (that is indeed a loop invariant) is strong enough to show the Hoare triple
-
Able to apply on larger more complicated programs (e.g., the
do_something
examples and in youria3
assignments) -
Practices:
- In-class examples
- In-class assignemtns (ia3)
Practice: come up with your own example (e.g., modify the
do_something
program or other in class examples) - Guess anincorrect
loop invariant and show that it is incorrect - Guess acorrect
loop invariant but not strong enough to prove the programs and show that it is correct but cannot prove the program - Guess acorrect
loop invairant and strong enough to prove the program and able to show that -
Abstract Interpretation
- Able to do the tabular method for various domains, e.g., odd/even,0 , neg/pos, interval
-
Focus on the detailed table method (i.e., your ia4 style).
- You do not need to do the "simplified" method I showed at the end as you can make lots of mistakes there. The table method seems to work well so I will only ask about this method.
-
Practices:
- In-class examples
-
In-class assignments (ia4)
-
Practice 1: Do the
mult
example in ia4 and themod
example in the class lecture - for every cases for the
Odd/Even/0
abstract domain (e.g., (A=even, B=odd), (A=even, B=even), ... - for the the interval domain (this can be challenging)
- Practice 2: come up with your own example (you can modify
mult
ormod
or other examples shown in class) and apply the following domains on it: Odd/Even/0
(case analysis, e.g., when inputs are odd, ...)Neg/Pos/0
(case analysis, e.g., when inputs are Neg, ..)Interval
Misc questions
- so far we only talk about verifying progarams with
while
loops- how you would convert other types of loops (
do ... while(g)
,for
) into awhile
loop.
- how you would convert other types of loops (
- What are the trade-offs in Hoare logic (e.g., pros/cons of proving Hoare triples)?
- What does it mean when we can prove a Hoare triple ? what does it mean when we cannot prove a Hoare triple ?
- What are the trade-offs in abstract interpretation (e.g., pros/cons)?