Generating Correct-by-Construction Code from Graphviz Diagrams
Stateful systems are extremely common in the real world: lift controllers, ATMs, even networks all have an underlying state which updates as the system receives different inputs. These stateful systems can be drawn as diagrams, and we show that it is possible to generate correct-by-construction code models of these systems from their diagrams.
Keywords
research, software design, state machines, software correctness, dependent types