ANNA : a language for annotating Ada programs : reference manual
This 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...
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Livre numérique |
| Sprog: | Anglais |
| Udgivet: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serier: | Lecture notes in computer science
260 |
| Fag: | |
| Online adgang: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Kommentar: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • ANNA, a language for annotating Ada programs, reference manual, David C. Luckham ... [et al.], 1987, Berlin, Springer-Verlag, 1 vol. (v-143 p.), Lecture notes in computer science, 0-387-17980-1 • ANNA A Language for Annotating Ada Programs, Texte imprimé, 9783662178461 |
| LEADER | 04146nam a22003857a 4500 | ||
|---|---|---|---|
| 001 | 944902 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155206516 | ||
| 020 | |a 9783540472025 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 082 | |a 005.13 | ||
| 100 | 1 | |a Luckham, David C. | |
| 245 | 1 | 0 | |a ANNA : |b a language for annotating Ada programs : reference manual |c David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner... [et al.]. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 260 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a 1. 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. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 520 | |a This 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 | |a Informatique | ||
| 650 | |a Langages de programmation | ||
| 700 | 1 | |a Henke, Friedrich W. von, |d 19..- |4 aut | |
| 700 | 1 | |a Krieg-Brückner, Bernd. |4 aut | |
| 776 | 0 | |0 020294190 |t ANNA, a language for annotating Ada programs |o reference manual |f David C. Luckham ... [et al.] |d 1987 |c Berlin |n Springer-Verlag |p 1 vol. (v-143 p.) |s Lecture notes in computer science |z 0-387-17980-1 | |
| 776 | 0 | |t ANNA A Language for Annotating Ada Programs |b Texte imprimé |z 9783662178461 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-17980-1 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-NPWJ6JWV-G |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:747915458 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-17980-1 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:750928093 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-17980-1 |z Accès INSA CVL | |
| 997 | |0 944902 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||