3 ms·
Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one o
by Joker_vD 6y ago
Right, the axiomatic semantics aka "the Floyd-Hoare rules". The interesting thing about them is that I've read many presentations of them and not a single one of those had any mention of subroutines (procedures or functions, doesn't matter) at all. All you have is global variables, assignments, sequencing, conditions, and loops. That's it. And while one would think that adding support for subroutines would be tremendously useful, allowing for e.g. specifying correctness of data structures' implementations, apparently it has not been done.
The closest thing to it I've seen is TLA+ but holy fatcats is it unwieldy.
- rssoconnor 6y agoVerifiableC[1] provides Hoare rules for (a large subset[2] of) C that include function calls, pointers and heap allocation, and some amount of concurrency. It does use an extension to Hoare logic, called separation logic, to achieve some of these features. In particular, separation logic's frame rule is instrumental for the modularization needed for semantics of function calls. [1]https://vst.cs.princeton.edu/veric/ https://vst.cs.princeton.edu/veric/ [2]excludes setjmp/longjmp, unstructured switch statements, goto and maybe a few other moderately exotic constructions.
- Joker_vD 6y agoNo goto? Funny, but there is actually a Hoare rule for goto (by Hoare himself), and a rather straightforward one: { pre(L) } S; { P } ------------------------ { pre(L) } L: S; { P } { pre(L) } goto L; { false } You just have to use the same precondition pre(L) for every mention of the label L.
- deleted 6y ago[deleted]