[User23]

As the author notes, Dijkstra's paper is a bit of a challenge, but it's well worth reading: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD07xx/E.... It's a great example of deriving an algorithm from a predicated acceptance state.