Declarations and Blocks
A programming language needs a way of introducing new identifiers, VDM-SL has three constructs for this purpose. Though the three constructs are based on the same definition, restrictions are placed on their use to give different semantics that assist with proof obligations, and thus the three constructs provide different facilities.
KeywordsLogical Constant Proof Obligation Post Post Local Identifier Informal Semantic
Unable to display preview. Download preview PDF.