In “Lua Source Code Appreciation”, it’s mentioned that Lua’s author Roberto drew partial inspiration from VDM when designing Lua, yet there’s very little Chinese documentation about VDM. Here I provide a simple Chinese version as a memo.
Wiki original https://en.wikipedia.org/wiki/Vienna_Development_Method
The Vienna Development Method (VDM) is one of the longest-established formal methods1 for the development of computer systems. Its origins were in work done at the IBM Vienna Laboratory in the 1970s. VDM has since evolved into a family of techniques and tools based on a formal specification language—the VDM Specification Language (VDM-SL). VDM also has an extended form: VDM++, which supports object-oriented and concurrent systems. Support for VDM includes tools for analyzing models in commercial and academic contexts, as well as testing and verification of models and code generation from VDM models. VDM has a history of industrial applications and research that continues to evolve, making notable contributions to the engineering of critical systems, compilers, concurrent systems, and logic in computer science.
Philosophy
In VDM-SL, computing systems can be modeled at a higher level of abstraction than programming language implementations, allowing analysis of designs and identification of key characteristics and flaws in the early stages of system development. Validated models can be transformed into detailed system designs through a refinement process. The language has a formal semantics, allowing properties of models to be proved at higher levels of abstraction. It also has an executable subset, enabling models to be analyzed through testing and displayed through graphical interfaces so that models can be evaluated by domain experts who are not familiar with the modeling language itself.
