by jayaprabhakar on 4/15/24, 12:52 PM with 1 comments
by jayaprabhakar on 4/15/24, 12:52 PM
This post is a follow up of https://ahelwer.ca/post/2023-03-30-pseudocode/
Where Andrew pointed compared executable Python code vs executable model checker PlusCal.
In this blog, I'm showing how to model check Python code with minor changes.
For the curious, model checking is the formal methods technique that explores every possible path to ensure the invariants are met in every case.