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.


Logical Constant Proof Obligation Post Post Local Identifier Informal Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag London Limited 1997

Authors and Affiliations

  • Derek Andrews
    • 1
  1. 1.Department of Mathematics and Computer ScienceLeicester UniversityLeicesterUK

Personalised recommendations