Hoare-Like Triples and Kleene Algebras with Top and Tests

on YouTube ↗23m

" summary

A taxonomy of program logics uses predicate transformers plus Kleene algebra with top and tests to show which Hoare-like triples are equationally definable. Partial correctness and incorrectness get simple top-cut equations; a Lisban/ Angelic weakest pre total-correctness equation also appears. New definitions of demonic strongest post and angelic strongest-liberal post fit the lattice but reveal an irreducible asymmetry: some expected duals are not expressible. Work continues on existential triples and when the picture collapses under termination or reversibility.

AI-written summary · about

" chapters (17)

1. 0:00Introduction
2. 0:20Program logics overview
3. 1:03Weakest precondition transformers
4. 2:50Angelic vs demonic transformers
5. 4:34Correctness triples
6. 6:42Strongest postcondition variants
7. 7:47Correctness symmetry
8. 8:30Kleene algebras introduction
9. 9:55Tests in relational algebra
10. 11:00Top for incorrectness
11. 11:42Partial correctness algebra
12. 13:08Angelic total correctness
13. 14:12Expressive properties summary
14. 15:17New transformers taxonomy
15. 17:01Forward vs backward asymmetry
16. 18:27Future work
17. 19:35Q&A