3 ms·
Yes, I will concede that of course PTS can be used in a "first the invariants, then the code" way, and so my distinction doesn't make much sense here. Neverthe
by practal 4y ago
Yes, I will concede that of course PTS can be used in a "first the invariants, then the code" way, and so my distinction doesn't make much sense here.
Nevertheless, PTS is for verifying imperative programs, and if whenever possible, I prefer reasoning about more elegant and simple mathematical objects instead.
- User23 4y agoI find a lattice of functions from a predicate to another predicate to be about as simple as possible for describing the problem space. I’ve still got a lot to learn, but given that state is a reality for the computing automata we can actually build I like an abstraction that captures it directly. I have found this to be an interesting exchange of ideas and I appreciate your taking the time to answer my queries. Thanks!