ISO/IEC JTC1/SC22/WG9 N360 Disposition of Comments on IEC/ISO TR 15942 Information technology - Programming languages - Guide for the Use of the Ada Programming Language in High Integrity Systems (Technical Report Type 3) Submitted by Brian Wichmann, 15942 project editor, 13 May 1999 in response to PDTR balloting Ballot result reference ISO/IEC JTC 1/SC22 N2893 Canadian 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. > Since the SC22 vote was 12 in favour with only one against, the response to the comments made are deliberately ultra-conservative. Only in those cases in which a clear textual change has been proposed, and the change has clear support, do we propose an actual change 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. We agree that the underlying hardware and the nature of the compiled code can impact the optimal approach to the development of high integrity systems. However, we cannot anticipate potential changes to hardware in the next 5 years, and hence propose no changes to the TR. Also issues such as the impact of cache on timing are well known. > 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. Agreed. The exclusion of human factors in 1.2 was supposed to be only the aspects associated with the application, rather than those arising from the software engineering using Ada. Proposed wording change: Change last bullet of 1.2 to read: 'Human factor issues in the application (as opposed to human factors in the use of the Ada language which is in scope).' > 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. Agreed. The text is not formatted as a Note. Proposed wording change: Delete 'Note: '. Also, replace 'where the modification is not intended' by 'where modification is not planned'. Also, replace the final words in the penultimate sentence from 'to facilitate testing, memory use analysis, etc' to 'to facilitate testing and analysis'. > 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. Agreed, although the standards includes security as well as safety. Proposed wording change: Replace 'standards' by 'applicable standards and guidelines (see Section 7.1)' > 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... This proposal is unclear as the referenced paragraph is not given explicitly. Surely call tree analysis is part of flow-control? No change is proposed. > 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. We agreed that there are cases in which the additional verification techniques for Allowed features are not specified with the precision that would be ideal. However, it seems there is no consensus for changing the wording of the definition of Allowed, since the general intent is stated. Practical experience in applying this Guide over the next five years should clarify the situation, at which point, a revised TR can be prepared. > 7. Section 5.1, paragraph 2 > The last sentence is inaccurate. Use an example of subprogram completion > or overriding primitive operations Agreed that the last sentence is inaccurate. Proposed to replace this by: 'When a compiler determines that a subprogram completion, such as a subprogram body or a renames of a subprogram, does not match the static subtype profile of the specification, it reports an error. In general, the concept of static expressions and subtypes enables many erroneous programs to be detected at compile-time rather than run-time. For example the component types of array types must statically match during conversion. Ada 95 enhances the already-rigorous static-matching rules of Ada 83.' > 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 > referred 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. Agreed that this is slightly confusing. Proposed wording change: Replace 'functional coverage' by 'a complete analysis'. > 9. Section 5.2.1, item 2. > What does "The use of discriminants in the creation of unconstrained > objects" mean? Precise terminology is defined in the ARM; it should be > used here. The wording uses the accords with the ARM, but with less precision to reflect the various implementation methods of compiling objects with discriminants. Hence no wording change in proposed. > 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. No change proposed and the intent is clear. > 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) We agree that the discussion on the simple case should be extended. However, the complexities typically relate to other language features such are representation clauses (see section 5.9), and therefore it is unclear where the issue is best addressed. No change is proposed at this point, but we anticipate that use of the TR will enable the revision to address this point adequately. > 12. Section 5.2.1 Item 6 > A classic example of the problem with the 3-way rating scale. What is the > workaround? Propose to add to the note (in 5.2.2, item 6) the following: 'Block statements can be avoided by replacing them by a parameterless subprogram.' > 13. Section 5.3.2 Note 1 > Remove "is excluded because it" (hinders Symbolic...). - Not needed > (minor point) No change is proposed. > 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. No change is proposed. > 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? Propose to add a sentence to the note: 'Therefore the use of such generics should be restricted to avoid these problems.' > 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. We do not think a change to the classification can be justified in view of the SC22 ballot result. In any case, the restrictions on dynamic types implies that the main cases in which TA and OCA would be troublesome are already excluded. > 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. Like point 12, we do not think it necessary to elaborate on a workaround for each feature which is marked 'Alld'. No change proposed. > 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. While we agree that there is some justification in the proposal made, no change is proposed since a wording change that would be a definite improvement could not be agreed. Hence no change is proposed. > 19. Section 5.4.3, paragraph 2, last two sentences. > How can an array be "heterogeneous"? The last sentence is cryptic; the > referents of "former" and "latter" are unclear. Propose deleting 'heterogeneous,' and replace 'former' by 'named aggregates' and 'the later' by 'others'. ('others' in bold, of course). > 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? Agreed that the wording need clarification, since the application should be re-coded to avoid the conversion which cannot be effectively validated. Replace the text 'the conversion should be coded explicitly, with look-up tables,' by 'the application should be recoded to avoid such conversions using, for instance, look-up tables,'... > 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. The point has been highlighted and no change is proposed. > 22. Section 5.5.3, paragraph 3. > We Do not believe this assertion. Replace the part of the sentence to the colon by: 'Function correctness of nested loops is facilitated if the following is true' > 23. Section 5.6.1 > We need an statement about recursion. Recursion appears to have been > missed as an evaluated capability. Add a note '10' to 5.6.2 with the text: 'For the implications of recursion, see the next section.'. Add this note number to both the features 'Procedures' and 'Functions' in table 5.6.1 (ie, the first column). In addition, the editor proposes to add all the occurrences of the word 'recursion' to the index. > 24. Section 5.6.2 Item 3 > If this note is correct, then this is "exc". This section needs more > thought. To clarify the wording, add to the second sentence: ', depending upon the implementation and the operations applied to the parameters.' > 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. This is a tricky area, since one does not wish to discourage the use of private types. the existing warning seems adequate, so no change is proposed. > 26. Section 5.7.1,2 Note 4 > This is a human factors issue and needs to be be eliminated. No change proposed. > 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. No change proposed. > 28. Section 5.9.2 Note 1 > If we can't do the analysis, what is the workaround? Suggest thorough > review. To clarify this point, add to the second paragraph of 5.9.3 the following: 'Careful human analysis of the generated object code of these features will usually be required to replace more traditional analysis forms.' > 29. Section 5.9.2 Item 7 > What is the workaround to support flow analysis - suggest annotations. No change proposed. > 30. Section 5.9.2 Item 10 > This clearly needs more discussion - Workarounds need to be provided - > Suggest annotated code and hand review of object code No change proposed. > 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 No change proposed. > 32. 5.10.2 Item 1 > This cannot be "alld" without a workaround. We do not think it necessary to elaborate on a workaround for each feature which is marked 'Alld', although this might be possible in a subsequent revision of this TR. No change proposed. > 33. 5.10.2 Item 2. > This item needs a workaround - suggestion - analyse the instance We do not think it necessary to elaborate on a workaround for each feature which is marked 'Alld', although this might be possible in a subsequent revision of this TR. No change proposed. > 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 No change proposed. > 35. Section 5.10.2 Item 4 > There is no static matching in generics No change proposed. > 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. This note is somewhat confusing and hence replace it by: 'For non library-level generic instantiations, each instance of an "in" object is non-static and requires an object of potentially unknown size to be created in the stack frame of the instantiating unit. Unlike library level instantiations which only allocate the storage once at program elaboration time, stack-based elaboration may change each time the enclosing unit is called.' > 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. We agree that further clarification is needed here. Add to the Table in 5.10.1, reference to Note 3 under the two entries which refer to Note 6. > 38. Section 5.10.2 - Item 7 > This is too cryptic to be useful. Unfortunately, the range of possible generic types is too large to provide effective advice in a reasonable number of words. However, two references provide additional material, so add: 'For further analysis, refer to [CAT3, AQS].' > 39. Section 5.10.2 Item 8 > This is a human factors issue - doesn't justify an "alld" rating. Unclear what is being requested. No wording change proposed. > 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 To clarify the issue, add to the sentence: ', see also 5.3.2, Note 3'. > 41. Section 5.11 > We Found this complete section very weak and negative. It needs a rewrite > to better explain the issues. Replace the last sentence of the first paragraph by: 'When access types are used in ways that create aliases and export aliases, then data analysis and formal analysis of the system that includes these objects becomes quite difficult.' Add new paragraph 2 as follows: 'Most unconstrained Ada types can only have constrained objects as their members, with well-known techniques to implement the bounds. Parameters of unconstrained types always have actual objects associated with them. With proper use of preconditions or similar techniques, absolute bounds can be established for such types.' > 42. Section 5.11 Third paragraph. > The last sentence is unclear. An unconstrained variant record ought not > "change shape" (whatever that means). Agreed. Proposed wording change: Replace 'they may change shape during program execution' by 'a change in their discriminants will change the usage of the storage allocated to the objects during program execution'. > 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. There is no consensus for this proposed change. > 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? Replace first sentence by: 'Control flow analysis of access-to-subprogram types is intractable in the general case. At present there is no known model of this capability to support Symbolic Analysis. Timing Analysis is intractable in general but can bounded by annotations and manual checks. Object Code Analysis is difficult but not intractable.' > 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. The point being stated is merely that the analysis is more complex than for statically-bound arrays. No wording change proposed. > 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. Do not agree. Ada is well-defined, but this definition deliberately leaves undefined some points...! No wording change proposed. > 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. In the penultimate paragraph of 5.12, replace 'is recommended' by 'is possible'. > 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". The point is that the 'same' language construct could be checked implicitly or explicitly making OCA difficult. No wording change proposed. > 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. Replace the note by: 'Raise statements from deeply nested scopes can be obscure and cause difficulties for Flow Analysis and Object Code Analysis.' > 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? To clarify the situation, add to the end of note 6: 'With careful coding, an exception handler can be made to establish a recovery state that is independent of the implementation-dependent state when the handler is invoked.' > 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). To clarify the situation add to the end of existing note: 'The propagation of an exception cannot guarantee the current machine state and state of the subprogram which raised the exception, as well as possibly global or accessed objects. These conditions make future Flow Analysis and Symbolic Analysis of the program intractable and other analysis difficult.' > -------------------- end of Canada comments ------------------------------ Entirely editorial changes proposed by Editor. 1. Page 28, second bulleted item in 5.8.3, add 'the Numerics Annex' after 'implementations that support'. 2. Page 43, references [CAT1], [CAT2] and [CAT3]: Replace 'Saatlink' by 'Saaltink'. 3. Ensure that all references to 'recursion' are in the index. 4. Ensure additional reference to ASIS is in index. 5. Page 26, Section 5.7.2, Note 3. Replace 'Derivations of' by 'Derivations from'. 6. Page 35, last sentence: Add full-stop. 7. Page v, third paragraph of Introduction, replace ', so for all choices' by '. Therefore for any choice' (better English!) 8. Page v, paragraph starting 'All language design', replace 'integrity, for' by 'integrity. For' (better English!) 9. Page v, paragraph starting 'There are, however, a', replace that text by: 'There are a'. (better English!). 10. Page 32, last two lines: 'in out' in bold on both lines. --- ------------------------------------------------------------- Brian Wichmann Tele: +44 181 943 6976 (direct) National Physical Laboratory FAX: +44 181 977 7091 Teddington Middlesex e-mail: brian.wichmann@npl.co.uk TW11 0LW UK (Typically only available on Tuesdays and Thursdays.) WWW: http://www.npl.co.uk/npl/cise/index.html The contents of the above message, unless explicitly stated otherwise, are my views alone and should not be taken as representing the views held by NPL Management Ltd. -------------------------------------------------------------