000 03711nam a22005175i 4500
001 978-3-540-47202-5
003 DE-He213
005 20160624102021.0
007 cr nn 008mamaa
008 121227s1987 gw | s |||| 0|eng d
020 _a9783540472025
_9978-3-540-47202-5
024 7 _a10.1007/3-540-17980-1
_2doi
050 4 _aQA76.7-76.73
050 4 _aQA76.76.C65
072 7 _aUMX
_2bicssc
072 7 _aUMC
_2bicssc
072 7 _aCOM051010
_2bisacsh
072 7 _aCOM010000
_2bisacsh
082 0 4 _a005.13
_223
245 1 0 _aANNA A Language for Annotating Ada Programs
_h[electronic resource] /
_cedited by David C. Luckham, Friedrich W. Henke, Bernd Krieg-Brückner, Olaf Owe.
260 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_c1987.
264 1 _aBerlin, Heidelberg :
_bSpringer Berlin Heidelberg,
_c1987.
300 _aV, 148 p.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v260
505 0 _a1. Basic Anna concepts -- 2. Lexical elements -- 3. Annotations of declarations and types -- 4. Names and expressions in annotations -- 5. Statement annotations -- 6. Annotation of subprograms -- 7. Package annotations -- 8. Visibility rules in annotations -- 9. Task annotations -- 10. Program structure -- 11. Exception annotations -- 12. Annotation of generic units -- 13. Annotation of emplementation-dependent features.
520 _aThis reference manual of ANNA is another volume addressed to the ADA community. ANNA is a language extension of ADA to include facilities for formally specifying the intended behavior of ADA programs. It is designed to meet a perceived need to augment ADA with precise machine-processable annotations so that well established formal methods of specification and documentation can be applied to ADA programs. The current ANNA design includes annotations of all ADA constructs except tasking. Similar extensions for formal specification can be made to other Algol-like languages such as Pascal, PL/1, Concurrent Pascal, and Modula; essentially, these extensions would be subsets of ANNA. The design of ANNA was undertaken from the beginning with four principal considerations: 1. Constructing annotations should be easy for the ADA programmer and should depend as much as possible on notation and concepts of ADA. 2. ANNA should possess language features that are widely used in the specification and documentation of programs. 3. ANNA should provide a framework within which the various established theories of formally specifying programs may be applied to ADA. 4. Annotations should be equally well suited for different possible applications during the life cycle of a program. Such applications include not only testing, debugging and formal verification of a finished program, but also specification of program parts during the earlier stages of requirements analysis and program design.
650 0 _aComputer science.
650 1 4 _aComputer Science.
650 2 4 _aProgramming Languages, Compilers, Interpreters.
700 1 _aLuckham, David C.
_eeditor.
700 1 _aHenke, Friedrich W.
_eeditor.
700 1 _aKrieg-Brückner, Bernd.
_eeditor.
700 1 _aOwe, Olaf.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783540179801
786 _dSpringer
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v260
856 4 0 _uhttp://dx.doi.org/10.1007/3-540-17980-1
942 _2EBK6002
_cEBK
999 _c35296
_d35296