Vienna Development Method (VDM)
In the Vienna Development Method (VDM) models consist of a rich representation of data on which a system operates, together with the functionality that should be executed on these data structures. Besides the internal data also external input/output data is considered in the models.
The functional behavior can be either defined abstract by pre- and postconditions or explicitly by specific state-based operations. The precise mathematical semantics of these definitions allows for a wide range of analyses, e.g. static analysis, testing or proof of properties of the sytem.