Calculational Design of [In]Correctness Transformational Program Logics by Abstr...
summary
Claims that transformational correctness and incorrectness logics are abstract interpretation of the relational semantics’ right-image transformer, covering both finite and infinite executions, and gives a calculational method to derive sound, complete proof systems by fixpoint abstraction. Builds strongest-postcondition and a new precondition (in)correctness logic, recovers Hoare-style loop rules via Park/fixpoint induction, handles nondeterminism and termination, and demonstrates why a static analyzer’s factorial false alarm arises from abstracted nontermination.
AI-written summary · about
chapters (18)
- 0:00East to West logic
- 1:06Natural relational semantics
- 3:35Angelic semantics and iteration
- 5:45Deductive systems and fixed points
- 7:55Strongest post condition logic
- 9:01Strongest invariant for loops
- 10:09Implication and consequence rules
- 11:53Fixed point induction
- 12:57Under-approximation and iteration
- 14:02Deriving proof rules
- 15:54Balancing triviality and complexity
- 16:58Taxonomy of logic combinations
- 17:40Factorial program analysis
- 18:27False alarms in incorrectness logic
- 19:32Correctness vs incorrectness logic
- 20:35Transformational logic as abstraction
- 21:18Q&A with Peter
- 25:37Closing remarks