1. 2

Refinement proofs are hard. Those on data seem to be harder than those on control flow. I found this looking for any automated methods of refining abstract specs to efficient code. The author also had a prior tool that efficiently synthesized things like Red-Black Trees:


Note: Tools like these can be combined with fully-formal methods of software development like B method (or Event-B) to do some of the hard, refinement steps. I’ll be looking for tools to handle each type of hard iteration automatically or semi-automatically. Idea being you pause, convert the Z/B/whatever logic to the tool, get the data structure, and include that back in Z/B/whatever as something assumed correct with specific conditions of use. Might work might not…