ISO_IEC_TR_15942_2000E.pdf

Reference numberISO/IEC TR 15942:2000(E)ISO/IEC 2000TECHNICALREPORTISO/IECTR15942First edition2000-03-01Information technology Programminglanguages Guide for the use of the Adaprogramming language in high integritysystemsTechnologies de linformation Langages de programmation Guidepour lemploi du langage de programmation Ada dans les systmes dehaute intgritISO/IEC TR 15942:2000(E)PDF disclaimerThis PDF file may contain embedded typefaces.In accordance with Adobes licensing policy,this file may be printed or viewed but shall notbe edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing.In downloading thisfile,parties accept therein the responsibility of not infringing Adobes licensing policy.The ISO Central Secretariat accepts no liability in thisarea.Adobe is a trademark of Adobe Systems Incorporated.Details of the software products used to create this PDF file can be found in the General Info relative to the file;the PDF-creation parameterswere optimized for printing.Every care has been taken to ensure that the file is suitable for use by ISO member bodies.In the unlikely eventthat a problem relating to it is found,please inform the Central Secretariat at the address given below.ISO/IEC 2000All rights reserved.Unless otherwise specified,no part of this publication may be reproduced or utilized in any form or by any means,electronicor mechanical,including photocopying and microfilm,without permission in writing from either ISO at the address below or ISOs member bodyin the country of the requester.ISO copyright officeCase postale 56?CH-1211 Geneva 20Tel.+41 22 749 01 11Fax+41 22 734 10 79E-mail copyrightiso.chWeb www.iso.chPrinted in Switzerlandii ISO/IEC 2000 All rights reservedISO/IEC TR 15942:2000(E)ISO/IEC 2000-All rights reservediiiContents1Scope.11.1Within the scope.11.2Out of scope.22Verification Techniques.22.1Traceability.22.2Reviews.32.3Analysis.32.3.1Control Flow analysis.42.3.2Data Flow analysis.42.3.3Information Flow analysis.42.3.4Symbolic Execution.42.3.5Formal Code Verification.52.3.6Range Checking.62.3.7Stack Usage analysis.62.3.8Timing Analysis.62.3.9Other Memory Usage analysis.62.3.10 Object Code Analysis.72.4Testing.72.4.1Principles.72.4.2Requirements-based Testing.72.4.3Structure-based Testing.82.5Use of Verification Techniques in this Technical Report.83General Language Issues.93.1Writing Verifiable Programs.93.1.1Language Rules to Achieve Predictability.103.1.2Language Rules to Allow Modelling.103.1.3Language Rules to Facilitate Testing.113.1.4Pragmatic Considerations.123.1.5Language Enhancements.123.2The Choice of Language.134Significance of Language Features for High Integrity.144.1Criteria for Assessment of Language Features.144.2How to use this Technical Report.145Assessment of Language Features.155.1Types with Static Attributes.165.1.1Evaluation.175.1.2Notes.175.1.3Guidance.175.2Declarations.175.2.1Evaluation.185.2.2Notes.185.2.3Guidance.185.3Names,including Scope and Visibility.195.3.1Evaluation.195.3.2Notes.195.3.3Guidance.205.4Expressions.205.4.1Evaluation.215.4.2Notes.215.4.3Guidance.22ISO/IEC TR 15942:2000(E)ISO/IEC 2000-All rights reservediv5.5Statements.225.5.1Evaluation.235.5.2Notes.235.5.3Guidance.235.6Subprograms.245.6.1Evaluation.245.6.2Notes.245.6.3Guidance.255.7Packages(child and library).255.7.1Evaluation.265.7.2Notes.265.7.3Guidance.265.8Arithmetic Types.275.8.1Evaluation.275.8.2Notes.275.8.3Guidance.285.9Low Level and Interfacing.295.9.1Evaluation.305.9.2Notes.305.9.3Guidance.315.10Generics.315.10.1 Evaluation.325.10.2 Notes.325.10.3 Guidance.335.11Access Types and Types with Dynamic Attributes.345.11.1 Evaluation.345.11.2 Notes.345.11.3 Guidance.355.12Exceptions.355.12.1 Evaluation.365.12.2 Notes.365.12.3 Guidance.365.13Tasking.375.13.1 Evaluation.395.13.2 Notes.395.13.3 Guidance.395.14Distribution.405.14.1 Evaluation.405.14.2 Notes.405.14.3 Guidance.406Compilers and Run-time Systems.406.1Language issues.416.2Compiler Qualification.416.3Run-Time System.427References.437.1Applicable Documents.437.2Referenced Documents.44ISO/IEC TR 15942:2000(E)ForewordISO(the International Organization for Standardization)and IEC(the International Electrotechnical Commission)form thespecialized system for worldwide standardization.National bodies that are members of ISO or IEC participate in thedevelopment of International Standards through technical committees established by the respective organization to deal withparticular fields of technical activity.ISO and IEC technical committees collaborate in fields of mutual interest.Otherinternational organizations,governmental and non-governmental,in liaison with ISO and IEC,also take part in the work.International Standards are drafted in accordance with the rules given in the ISO/IEC Directives,Part 3.In the field of information technology,ISO and IEC have established a joint technical committee,ISO/IEC JTC 1.DraftInternational Standards adopted by the technical committees ar