Principles of Program Engineering

Compiled by Robert "Corky" Cartwright

• Notes on Object-Oriented Design (pdf)
• Notes on Object-Oriented Design (postscript)
• Notes on Object-Oriented Design (html)
• Hoare's Logic Part1
• Hoare's Logic Part2
• Sample Proof in Hoare's Logic
• Proof Sketch involving arrays in Hoare's Logic
• Paper on First Order Programing Logic
• Notes on First Order Programing Logic
• Sample Proof in FOPL
• Notes on Reasoning about Higher Order Data
• Notes on type systems I
• Notes on type systems II
• Notes on type systems III
• Notes on type systems IV
• Notes on type systems V
• Typing Rules for IPLC
• Comp 607: Automated Program Verification (by Ian Barland, Moshe Vardi, and John Greiner)
• Model Checking Concurrent Programs (by Ian Barland, Moshe Vardi, and John Greiner)
• SPIN: On-the-Fly LTL Model Checking
• Spin Implementations of the "Dining Philosophers" (by Mathias Ricken):
  1. Failed attempt: No locks
  2. Failed attempt: No locks, with assertions that show the errors
  3. Failed attempt: A lock for every fork
  4. Failed attempt: A lock for every other fork
  5. Successful attempt: Locks acquired in total order, released in reverse order
  6. Successful attempt: Locks acquired in total order, released in same order
• Doug Lea's "Concurrent Programming in Java" Online Book Supplement