From rinehuls@Radix.Net Thu Mar 11 22:39:49 1999 Received: from mail1.radix.net (mail1.radix.net [209.48.224.31]) by dkuug.dk (8.8.7/8.8.7) with ESMTP id WAA11656; Thu, 11 Mar 1999 22:39:44 +0100 (CET) (envelope-from rinehuls@Radix.Net) Received: from saltmine.radix.net (saltmine.radix.net [209.48.224.40]) by mail1.radix.net (8.9.1/8.9.1) with SMTP id QAA16275; Thu, 11 Mar 1999 16:39:44 -0500 (EST) Date: Thu, 11 Mar 1999 16:39:42 -0500 (EST) From: William Rinehuls To: sc22docs@dkuug.dk cc: Jim Moore , keld simonsen Subject: SC22 N2893 - Vote Summary of LB N2835 - PDTR 15942 - Ada Guide inHigh Integrity Systems Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII _________________ beginning of title page __________________________ ISO/IEC JTC 1/SC22 Programming languages, their environments and system software interfaces Secretariat: U.S.A. (ANSI) ISO/IEC JTC 1/SC22 N2893 TITLE: Summary of Voting on PDTR Ballot for PDTR 15942: Information technology - Programming languages - Guide for the Use of the Ada Programming Language in High Integrity Systems (Technical Report Type 3) DATE ASSIGNED: 1999-03-09 SOURCE: Secretariat, ISO/IEC JTC 1/SC22 BACKWARD POINTER: N/A DOCUMENT TYPE: Summary of Voting PROJECT NUMBER: JTC 1.22.15942 STATUS: WG9 is requested to prepare a Disposition of Commments Report and make a recommendation on the further processing of the PDTR. ACTION IDENTIFIER: FYI to SC22 Member Bodies ACT to WG9 DUE DATE: N/A DISTRIBUTION: Text CROSS REFERENCE: N2835 DISTRIBUTION FORM: Def Address reply to: ISO/IEC JTC 1/SC22 Secretariat William C. Rinehuls 8457 Rushing Creek Court Springfield, VA 22153 USA Telephone: +1 (703) 912-9680 Fax: +1 (703) 912-2973 email: rinehuls@radix.net _________ end of title page; beginning of overall summary _______________ SUMMARY OF VOTING ON Letter Ballot Reference No: SC22 N2835 Circulated by: JTC 1/SC22 Circulation Date: 1998-11-24 Closing Date: 1999-03-08 SUBJECT: PDTR Ballot for PDTR 15942 - Information technology, Programming languages - Guide for the Use of the Ada Programming Language in High Integrity Systems (Technical Report Type 3) ------------------------------------------------------------------------- The following responses have been received on the subject of approval: "P" Members supporting approval without comment 12 "P" Members supporting approval with comment 0 "P" Members not supporting approval 1 "P" Members abstaining 3 "P" Members not voting 6 "O" Members supporting approval without comment 1 "O" Members abstaining 1 ------------------------------------------------------------------------ Secretariat Action: WG9 is requested to prepare a Disposition of Comments Report and make a recommendation on the further processing of the PDTR. The comment accompanying the abstention vote from Austria was: "Lack of expert resources." The comment accompanying the abstention vote from Denmark was: "Due to lack of Danish expertise". The comment accompanying the abstention vote from France was: "Due to lack of resources." The comment accompanying the abstention vote from Sweden was: "Due to lack of expertise." The comments accompanying the negative vote from Canada are attached. ____________ end of overall summary; beginning of detail summary ______ ISO/IEC JTC1/SC22 LETTER BALLOT SUMMARY PROJECT NO: JTC 1.22.15942 SUBJECT: PDTR Ballot for PDTR 15942 - Information technology - Programming languages - Guide for the Use of the Ada Programming Language in High Integrity Systems (Technical Report, Type 3) Reference Document No: N2835 Ballot Document No: N2835 Circulation Date: 1998-11-24 Closing Date: 1999-03-08 Circulated To: SC22 P, O, L Circulated By: Secretariat SUMMARY OF VOTING AND COMMENTS RECEIVED Approve Disapprove Abstain Comments Not Voting 'P' Members Australia (X) ( ) ( ) ( ) ( ) Austria ( ) ( ) (X) (X) ( ) Belgium ( ) ( ) ( ) ( ) (X) Brazil ( ) ( ) ( ) ( ) (X) Canada ( ) (X) ( ) (X) ( ) China ( ) ( ) ( ) ( ) (X) Czech Republic (X) ( ) ( ) ( ) ( ) Denmark ( ) ( ) (X) (X) ( ) Egypt ( ) ( ) ( ) ( ) (X) Finland (X) ( ) ( ) ( ) ( ) France ( ) ( ) (X) (X) ( ) Germany (X) ( ) ( ) ( ) ( ) Ireland (X) ( ) ( ) ( ) ( ) Japan (X) ( ) ( ) ( ) ( ) Netherlands (X) ( ) ( ) ( ) ( ) Norway (X) ( ) ( ) ( ) ( ) Romania ( ) ( ) ( ) ( ) (X) Russian Federation (X) ( ) ( ) ( ) ( ) Slovenia ( ) ( ) ( ) ( ) (X) UK (X) ( ) ( ) ( ) ( ) Ukraine (X) ( ) ( ) ( ) ( ) USA (X) ( ) ( ) ( ) ( ) 'O' Members Voting Korea Republic (X) ( ) ( ) ( ) ( ) Sweden ( ) ( ) (X) (X) ( ) _________ end of detail summary; beginning Canada comments _____________ Comments Accompanying Canada "No" vote. We vote no on this document in its present state. In general we find the goal and intent of the document appropriate, but have a number of reservations and technical comments. If these comments are resolved to our satisfaction we would vote yes to the document. 1. Section 2. A number of times assumptions are made about the general applicability of a method or kinds of analysis that is done is only possible in the context of a specific implementation - for example, on a SPARC system, register spillage onto the stack can adversely impact stack-usage and timing analysis (e.g., whether a procedure is implemented as a "leaf" of not matters). Issues like caching can also have significant impact on timing. Also, many features have known good implementation strategies, but one cannot assume that an implementation chose that strategy. Clear statements that the analysis assumes standard implementation strategies and appropriate implementation behaviour is needed as a caveat in section 2. The ratings are "learned opinion" based on typical implementations, but new hardware and compiler technology could lead to different ratings. 2. Section 1.2 says that human factors are not an issue, but a number of places downrate language features based on complexity for humans. Either need to explicitly include human factors like complexity and put into the rating scale (engineering), or eliminate these negative ratings Suggest for these cases leaving rating intact (as Inc) but flagging the human factors issue in the note. A possible exception might be under OCA, where the application of human review can be affected by these factors. If so, the scope statement of 1.2 should be revised to account for it. 3. Section 1.1 The final note on tools that generate Ada code - Notes are non-normative. This should be restructured as normative text. Also, get rid of "etc" in 2nd last line. 4. Section 2.0 Verification Techniques, paragraph 2 The statement talks about 4 approaches required by standards - specify what kind of standards - standards for the development of safety-related software is our presumption. 5. Section 2.3.1 - paragraph 3 This doesn't relate to control-flow analysis, the topic of the section Suggested wording Although most languages have the same flow control structures, specifics about the way that they are implemented can significantly enhance the structure, analysability and formal analysis of the code. For example, the Ada restriction on the modification of the for loop variable greatly simplifies loop analysis, especially the loop termination problem. If the goto... 6. Section 4.1. The three way classification for criteria (included, allowed, excluded) scheme blurs the distinction between two senses of the term "Allowed". If this scheme is going to be retained, the then for each feature where an "alld" appears must indicated whether verification is difficult or impossible, and if impossible, what are the techniques to "effectively circumvent" the use of the verification technique. Section 4.2 refers to these "additional verification steps for allowed features", so it is clear that readers need to know what they are. The places where we do not believe that this is yet done will be specifically commented. 7. Section 5.1, paragraph 2 The last sentence is inaccurate. Use an example of subprogram completion or overriding primitive operations 8. Section 5.1.2, item 2. Does "functional coverage" mean OCA? If not, what does it mean? The report should adhere to a consistent terminology in the notes. Item 2 is refered to in the "Allowed" rating for SA, but does not indicate what the difficulty is. Is there, in fact, a problem here? ASIS-based SA tools should not have any difficulty with derivation. 9. Section 5.2.1, item 2. What does "The use of discriminants in the creation of unconstrained objects" mean? Precise tereminology is defined in the ARM; it should be used here. 10. Section 5.2.1 Item 3 The note should specifically indicate that the feature being considered here IS ONLY static initialisation. Need a rating for non-static initialisations. 11. Section 5.2.1 Item 4 Aliased objects, simple case - need to spell out what the simple case is, or point to somewhere that discusses it (such as CAT1 or the AIs) 12. Section 5.2.1 Item 6 A classic example of the problem with the 3-way rating scale. What is the workaround? 13. Section 5.3.2 Note 1 Remove "is excluded because it" (hinders Symbolic...). - Not needed (minor point) 14. Section 5.3.2 Note 2 This is a human factors issue and can't be supported. Rating is not supported at this point in time. 15. Section 5.3.2 - Note 3 Another example of the 3-way rating issue."Alld" is not justified unless a workaround can be provided. What is the workaround? 16. Section 5.4.1 Operators with Composite Operands - TA and OCA should be "Alld". Also note in 5.4.2 needs to provide workaround. 17. Section 5.4.2 Note 3 Another example of the 3-way rating issue. "Alld" is not justified unless a workaround can be provided. workarounds need to be specified. 18. Section 5.4.2 Note 5. The problems raised here do not justify the "alld" rating. This needs separation into 2 rows - one where we can justify the "alld" rating, with workarounds as appropriate, and the other an "exc" rating. 19. Section 5.4.3, paragraph 2, last two sentences. How can an array be "heterogenous"? The last sentence is cryptic; the referents of "former" and "latter" are unclear. 20. Section 5.4.3, paragraph 3, last bullet. How is an access type to be coded explicitly with a lookup table, function call, or case statement? 21. Section 5.5.2 Item 4. This section needs to specify the workaround - suggest - evaluate compiler code, if this happens, switch to loop/exit strategy. 22. Section 5.5.3, paragraph 3. We Do not believe this assertion. 23. Section 5.6.1 We need an statement about recursion. Recursion appears to have been missed as an evaluated capability. 24. Section 5.6.2 Item 3 If this note is correct, then this is "exc". This section needs more thought. 25. Section 5.7.1, 5.7.2 Note 3 There is too much wrapped here around private. Another entry which considers the complex usages of private is needed, such as private types with public and private primitive subprograms. 26. Section 5.7.1,2 Note 4 This is a human factors issue and needs to be be eliminated. 27. Section 5.8.1. Modular types are "allowed" under SA and RC, but the discussion in note 1 does not justify this. Since the semantics are clearly defined, SA and RC should not be impeded. 28. Section 5.9.2 Note 1 If we can't do the analysis, what is the workaround? Suggest thorough review. 29. Section 5.9.2 Item 7 What is the workaround to support flow analysis - suggest annotations. 30. Section 5.9.2 Item 10 This clearly needs more dicusssion - Workarounds need to be provided - Suggest annotated code and hand review of object code 31. Section 5.9.3 paragraph 2 Also discuss other ways of showing the use of the representation clauses is safe, such as annotation system or hand OCA 32. 5.10.2 Item 1 This cannot be "alld" without a workaround. 33. 5.10.2 Item 2. This item needs a workaround - suggestion - analyse the instance 34. 5.10.3 Item 3 Need a workaround, such as enforce additional restrictions with annotations and/or analyse the object code of each instance. What about symbolic analysis for this - in generics, nothing is static 35. Section 5.10.2 Item 4 There is no static matching in generics 36. 5.10.2 Item 5 Here the discussion is wrong. Generic data space for library-level instantiations goes into global data space - no problem. 37. Section 5.10.2 Item 6 This is a serious issue and needs a workaround to justify the rating We suggest annotations or OCA of the actual instantiation. 38. Section 5.10.2 - Item 7 This is too cryptic to be useful. 39. Section 5.10.2 Item 8 This is a human factors issue - doesn't justify an "alld" rating. 40. Section 5.10.2 Item 11 The note is inappropriate. We agree with the ratings for nested generics but the note needs better discussion. Nesting of generic instances - should be "alld" same as nested subprograms 41. Section 5.11 We Found this complete section very weak and negative. It needs a rewrite to better explain the issues. 42. Section 5.11 Third paragraph. The last sentence is unclear. An unconstrained variant record ought not "change shape" (whatever that means). 43. Section 5.11.1 We do not think full access types should be excluded for SA. Ways of verifying programs using pointers have been known for many years. 44. Section 5.11.2 Note 5 This note is cryptic. How is control flow "disrupted"? Is it perhaps meant that control flow analysis is made intractible? What are the "static locations and linker tools" referred to here? 45. Section 5.11.1 Non-static array objects can be included for SA. We do not think there is any problem; certainly note 8 does not indicate one. 46. Section 5.12 The first sentence of the first paragraph and the second sentence of the second paragraph are contradictory. We think the latter is more accurate; this is one area where the Ada semantics are quite loose. 47. Section 5.12 Further explanation should be included in the second to last paragraph. Recommending the suppression of exceptions seems remarkable, and can be supported only when there has been a thorough check that the conditions corresponding to the exceptional situations can never occur. 48. Section 5.12.1. Note 3 is unconvincing. Surely there are many language features with more than one possible implementation technique. That should not in itself be a reason to claim OCA is "difficult". 49. Section 5.12.2 Note 5 The "Alld" rating for raising user exceptions under FA and SA is not justified by the note. This should probably be "Inc". Similarly for handlers for user-defined exceptions. 50. Section 5.12.2 Note 6 This note supports an "Alld" rating, and indicates that the corresponding analysis is "intractable". Is there a method for "effectively circumventing" the analysis? 51. Section 5.12.2 Note 10 This note seems incorrect. Verification techniques that handle propagation of exceptions have been known for many years (e.g., from the Gypsy verification system). -------------------- end of Canada comments ------------------------------ ________________________ end of SC22 N2893 ____________________________