LEADER 04027nam 22005295 450 001 996465705703316 005 20200706040606.0 010 $a3-540-47202-9 024 7 $a10.1007/3-540-17980-1 035 $a(CKB)1000000000230635 035 $a(SSID)ssj0000321303 035 $a(PQKBManifestationID)11283921 035 $a(PQKBTitleCode)TC0000321303 035 $a(PQKBWorkID)10262867 035 $a(PQKB)11208571 035 $a(DE-He213)978-3-540-47202-5 035 $a(PPN)155206516 035 $a(EXLCZ)991000000000230635 100 $a20121227d1987 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aANNA A Language for Annotating Ada Programs$b[electronic resource] $eReference Manual /$fby David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brueckner, Olaf Owe 205 $a1st ed. 1987. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1987. 215 $a1 online resource (V, 148 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v260 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-17980-1 327 $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. 330 $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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v260 606 $aProgramming languages (Electronic computers) 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 615 0$aProgramming languages (Electronic computers). 615 14$aProgramming Languages, Compilers, Interpreters. 676 $a005.13 700 $aLuckham$b David C$4aut$4http://id.loc.gov/vocabulary/relators/aut$0999667 702 $aHenke$b Friedrich W. von$4aut$4http://id.loc.gov/vocabulary/relators/aut 702 $aKrieg-Brueckner$b Bernd$4aut$4http://id.loc.gov/vocabulary/relators/aut 702 $aOwe$b Olaf$4aut$4http://id.loc.gov/vocabulary/relators/aut 906 $aBOOK 912 $a996465705703316 996 $aANNA A Language for Annotating Ada Programs$92830598 997 $aUNISA