Skip to content

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 or False, 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 precondition P and show/prove that the verification condition is correct (i.e., show the program is correct wrt to given P and Q)
  • 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 your ia3 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 an incorrect loop invariant and show that it is incorrect - Guess a correct loop invariant but not strong enough to prove the programs and show that it is correct but cannot prove the program - Guess a correct 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 the mod 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 or mod 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 a while loop.
  • 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)?