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.
Unable to display preview. Download preview PDF.