ANSI INCITS ISO IEC 13817-1-1996 Information technology - Programming languages their environments and system software interfaces - Vienna Development Method - Specification Langua.pdf

1、INTERNATIONAL STANDARD ISO/IEC 13817-I First edition 1996-l 2-l 5 Information technology - Programming languages, their environments and system software interfaces - Vienna Development Method - Specification Language - Part 1: Base language Technologies de /information - Langages de programmation, l

2、eurs environnements et interfaces logiciel systkme - M ULD-2 was the name applied to the IBM Hursley contribution to this effort - the language itself was being developed mainly from Hursley along with the early compilers; ULD-1 was a term applied to the natural language description of the language)

3、. The description of PL/I in ULD-3 style ran through three versions. These are very large documents. Operational semantics is now seen as unnecessarily complicated as compared to denotational semantics. However, to make the principles of denotational semantics applicable to a language like PL/I with

4、 arbitrary transfer of control, procedures as arguments, complicated tasking, etc. required major theoretical break-throughs and a considerable mathematical apparatus not available at the time. The effort of the formal definition uncovered many language problems early and had a substantial influence

5、 on the shape of the language. Towards the end of the 1960s serious attempts were made to use the ULD-3 description as the basis of compiler designs. Many problems were uncovered: in general, one could say that the over-detailed mechanistic features of the operational semantics definition considerab

6、ly complicated the task of proving that compiling algorithms were correct. But again one should be clear that the work was a technical achievement: a series of papers was published that described how various programming language concepts could be mapped into implementations which could be proved cor

7、rect from the description (e.g. in JL71). I n addition, a series of proposals was made which could simplify the task of developing compilers from a semantic description. One of these was an early form of an exit construct (HJ70) which led to an interesting difference between the Vienna flavour of de

8、notational semantics and that used in Oxford. Another VDM-like idea that arose at this time was Peter Lucas twin machine proof (Luc68), and subsequently the observation that the ghost variable treatment in the twin machine could be replaced by retrieve functions (Jon70) as a simpler way of proving m

9、ost cases of data development are correct. It is worth noting that Lucas twin machine idea has been re-invented several times since: the generalization of retrieve functions to relations can be seen as equivalent to twin machines with invariants. Hans BeckiE spent some time in England with Peter Lan

10、din at Queen Mary College and was the person who first pushed the Vienna group in the direction of denotational semantics. (Until his untimely death in 1982, Hans Beckic )This is not intended to be a history of the Vienna Laboratory: citations are limited to those concerning VDM itself. xii ISO/IEC

11、13817-1 : 1996(E) had published relatively little of his scientific research; some of his important papers were published posthumously in Bek84.) Another crucial stimulus was the visit to the Vienna laboratory by Dana Scott in 1969 (see dBS69). During the period from 1971 to 1973, the Vienna group w

12、as diverted into other activities not really related to formal description. Cliff Jones at this time went back to the Hursley Laboratory and worked on a functional language description (ACJ72) and other aspects of what has become known as VDM. In particular he published a development of Earleys reco

13、gniser (Jon72) which is one of the first reports to use data reification. In late 1972 and throughout 73 and 74 the Vienna group (Cliff Jones returned and Dines BjGrner was recruited) had the opportunity to work on a PL/I compiler for what was then a very novel machine architecture. They of course d

14、ecided to base their development for the compiler on a formal description of the programming language. PL/I was then undergoing ECMA/ANSI standardization (ANS76). The Vienna group chose to write a denotational semantics for PL/I (BBHf74); this is the origin of the VDM) work on language description t

15、echniques. During the same period, at the IBM Laboratory in Hursley, an investigation into the use of Meta-IV to formaliy describe five of the major languages supported by IBM was carried out. The languages were PL/I, BASIC, FORTRAN, APL and COBOL. Sketches for parts of FORTRAN and APL were written,

16、 and a full description of minimal BASIC was produced. This work ceased when the language work was moved from Hursley. Cliff Jones and Dines Bjgrner took upon themselves the task of making sure that something other than technical reports existed to describe the work that had gone on on the language

17、aspects of VDM: Be78 is a first book-length description of that work. In ESRI, Cliff *Jones also developed the work on those aspects of VDM not specifically related to compiler development and the first book on what is now generally thought of as VDM is Jon80. Both of these books have now been super

18、ceded: the language description work is best accessed in Be82 and - in its second edition the non-language work is best seen in Jon90 and also in AI91. Within IBM, from 1978, a number of projects used VDM (for other than language descriptions). It was during this period that specifications of severa

19、l large systems were carried out at the Biiblingen Laboratory. (These included a file system for DOS and an fault report tracking system; a data reification for the file system was attempted to show that the proof techniques were viable in an industrial environment.) This work was carried out as par

20、t of a technology transfer program. Later the IBM Program Product Development Centre in Rome became involved, and work was done to formally specify a hotel management system. This work showed that VDM was suitable for large-scale projects; unfortunately little has been published on this experience.

21、Dines Bjarners group at the Technical University of Denmark strenuously pursued the use of VDM for language description and he and his colleagues were responsible for descriptions of the CHILL programming Language and a major effort to document the semantics of the Ada programming language (B080). L

22、anguage work was also continued at Leicester University where a formal definition of the full Pascal language was writ- ten (AH82) and later a formal definition of the programming language Modula-2, which became a Draft International Standard (AeWO). The non-language, specification, aspects of VDM w

23、ere taken up by the STL laboratory in Harlow and, partly because of their industrial push, the British Standards Institute (BSI) was persuaded to establish a standardization activity. This activity has not been easy because of the differences between the pressures of those interested in the language

24、 description aspects of VDM and those who are more interested in pre- and post-conditions, data reification and operation decomposition. It is to the credit of both the BSI and IS0 Standards committee that they have managed to bear in mind the requirements of both types of user and come up with a st

25、andard that embraces such a wide scope of technical ideas. STL was responsible for funding the first formal semantics of VDM-SL and the work that was done at Manchester University by Brian Monahan (Mon87) wa5 used as the starting point of the formal description of the specification language. A new f

26、ormal description based on this work was produced because of the necessity of merging together the two aspects of the specification language. The outcome of the standardization effort initiated by STL through the British Standards Institution (BSI) was the formation of a panel (BSI IST/5/-/50) w h o

27、se membership was also open to participants from non-British organizations. )It is worth getting some acronyms sorted out: VDL stands for Vienna Description Language and was a term used to describe the operational semantics (ULD-3) notation; VDM stands for Vienna Development Method and relates to th

28、e post-1973 work; the specification language part, of VDM is sometimes known as Meta-IV; it is now known as VDM-SL. . . . Xl11 ISO/IEC 13817-1 : 1996(E) In 1991 the need for a VDM-SL standard was also recognized by ISO/IEC JTC12) by the formation of a Working Group, SC22/WG19. The actual work on the

29、 standard is done by the members of the BSI Panel. Work on the Standard encouraged the building of computer-based tools to support both the language and the deve- lopment method. Adelard produced SpecBox, a tool that provided syntax and type checking of VDM specifications. Manchester University and

30、the Rutherford Appleton Laboratories wrote mural (JJLMSl), a prototype tool that supports both the specification language and the development method, providing a proof engine to help with data reification and operation decomposition. The Technical University of Denmark and the National Physical Labo

31、ratory have configured the Cornell Synthesizer (a structured editor tool) to support VDM-SL with some type-checking fa- cilities - this tool was used to produce the static semantics of VDM-SL. IFAD have produced a tool for syntax and type checking together with an interpreter for an executable subse

32、t to allow rapid prototyping. During its history, the Vienna Development Method, together with its specification languages has had a profound influence on both the specification of programming languages and the specification and development of systems. The ideas in VDM have influenced several other

33、specification languages including RAISE, COLD-K and VVSL. 2, Joint Technical Committee 1 of the International Standards Organization and the International Electra-technical Commission xiv INTERNATIONAL STANDARD 0 ISO/IEC ISO/IEC 13817-1:1996(E) Information technology - Programming languages, their e

34、nvironments and system software interfaces - Vienna Development Method - Specification Language - Part 1: Base language 1 Scope This part of ISO/IEC 13817 specifies the model based specification language VDM-SL (Vienna Development Method - Specification Language). It specifies: - two representations

35、: the mathematical and interchange; - the syntax; the static semantics: - the dynamic semantics; conformity for specifications and tools. It does not specify: -. the proof obligations; - the reification rules; the size or complexity of a specification that will exceed the capacity of any specific da

36、ta processing system or the capacity of a particular tool, nor the actions to be taken when the corresponding limits are exceeded; - the minimal requirements of a data processing system that is capable of supporting an implementation of a tool; the method that tools use for reporting errors. ISO/IEC

37、 13817-1 : 1996(E) 2 Normative References The following standards contain provisions which, through reference in this text, constitute requirements of this part of ISO/IEC 13817. At the time of publication, the editions indicated were valid. All standards are subject to revision, and parties to agre

38、ements based on this part of ISO/IEC 13817 are encouraged to investigate the possibility of applying the most recent editions of the standards indicated below. Members of IEC and IS0 maintain registers of currently valid International Standards. IS0 8859-1:19871), Information processing - g-bit sing

39、le-byte coded graphic character sets - Part 1: Latin alphabet No. 1. ISO/IEC 14977:1996, Syntactic Metalanguage - Extended BNF. 1) Currently under revision. 2 ISO/IEC 13817-1 : 1996(E) 3 Definitions For the purposes of this part of ISO/IEC 13817, the following definitions apply. 3.1 conforming speci

40、fication: A specification which is written in the language defined by this part of ISO/IEC 13817 and which obeys the conformity clauses for specifications in this part of ISO/IEC 13817. 3.2 conforming tool: A tool which processes conforming specifications and which obeys the conformity clauses for t

41、ools in this part of ISO/IEC 13817. 3.3 consistent specification: A specification that satisfies either the mathematical or interchange concrete syntax and can be translated by the syntax mapping into a representation that uses the core abstract syntax and for which the dynamic semantics defines at

42、least one model. 3.4 core abstract syntax: The core abstract syntax gives a second abstract version of the underlying structure of the language that uses a reduced number of constructs. Translation between the outer abstract syntax and the core abstract syntax is, (in general) explicitly defined by

43、a mapping function (see clause 12). In a few cases, where the core abstract syntax is not clearly related to the outer abstract syntax, translation or technical notes (annotations) are used to explain the translation. 3.5 dynamic semantics: Dynamic semantics are the rules for the derivation of the m

44、odels of a specification that satisfies either the mathematical or interchange concrete syntax and can be translated by the mapping function into a representation that uses the core abstract syntax. The dynamic semantics are expressed using a mathematical notation that is defined in clause 5. The me

45、aning of a consistent specification is given by a set of models that the specification defines. 3.6 error: A fault in a specification which means the specification could be a meaningless specification or the specification is inconsistent. 3.7 extension: An addition to the requirements of this part o

46、f ISO/IEC 13817 that does not invalidate any specification conforming with this standard except by prohibiting the use of one or more particular spellings of identifiers. This implies that any new semantic definitions that are introduced must be be consistent with those in this part of ISO/IEC 13817

47、. 3.8 inconsistent specification: A specification that is not consistent - the set of models defined for the specification as defined by the dynamic semantics is empty. 3.9 interchange concrete syntax: The interchange concrete syntax is an alternative set of lexical rules from the Lexis (see clause

48、9.7) the representation of which uses standard symbols. 3.16 mathematical concrete syntax: The mathematical concrete syntax is a set of grammatical rules defining the syntactic structure of the language in terms of other concrete syntax rules, or lexical rules from the Lexis (see clause 9.7). 3.11 m

49、eaningless specification: A specification which cannot be translated by the syntax mapping to the core abstract syntax and thus for which no semantics can be given. 3.12 model: A mathematical construction designated as the meaning of a specification (or part of such specifi- cation) as defined by the dynamic semantics. 3.13 outer abstract syntax: The outer abstract syntax gives an abstract version of the underlying structure of the language. Translation between the concrete and abstract syntax is implicit. In a few cases, where the abstract syntax is not clearly related to