Formal specification to code

This family is not a graphical language, but it is the other half of “diagrams into executable specifications.” A formal description — algebraic, model-based, or a software-spec modeling language — is compiled into source, executables, or circuit processing pipelines.

US5101491 (1992) is an early “synthesize, generate and check software from a formal description.” The Automatic Software Production cluster (US7278130 and continuations) industrializes model-driven generation of information systems and UIs. Later grants cover analytical software design, pattern matching in procedure verification, and processing a formal specification of a digital circuit.

The Chinese grant CN112306470B sits at the synchronous-language end: transform and automatically verify complex synchronous programs — the same intellectual neighborhood as Lustre/SCADE, which themselves compile diagrams and equations onto embedded targets.

A compiler that takes a diagram plus a formal spec and emits proven CPU or FPGA code inherits prior art from both this stack and the LabVIEW/Simulink stacks.