220.127.116.11 Mathematical Specification
/Baader, 1990/ section II, chap. 1.2 (here: "operational specification")
The Mathematical Specification is a formal specification defining the behavior of operations by the description of pre- and postconditions.
The postcondition describes the states that are allowed to be reached after the execution of the operation if the precondition was valid before the execution of the operation.
The Mathematical Specification may be applied for the description of operations on every level of abstraction.
There are interfaces to DVER - Design Verification, PVER - Program Verification and ACC - Analysis of Covert Channels.
- not applicable -
||Basic features of formal methods as a stock-taking of tools and concepts|
||Manual of the conference VDM '90; main emphasis is put on actual topics with regard to the formal specification languages VDM and Z
||Several specification topics, principles and characteristics for a good specification, several specification methods, the application of formal specification techniques in practice are discussed|
||Specification in Z|
||Describes VDM and its basis|
||Several reports on "formal specification and verification"|
||Deals with temporal logic and verification of statements in temporal logic
||Last Updated 01.Jan.2002