From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,611f4b10cbf9af69 X-Google-Attributes: gid103376,public From: dgibson@cayman.cis.ohio-state.edu (david scott gibson) Subject: Re: Redefinition of Equality Date: 1996/10/04 Message-ID: <5335rjINNcdb@cayman.cis.ohio-state.edu>#1/1 X-Deja-AN: 187567746 references: <52hgmoINN7tg@snoopy.cis.ohio-state.edu> <324FD267.954@cis.ohio-state.edu> organization: The Ohio State University, Department of Computer and Information Science newsgroups: comp.lang.ada Date: 1996-10-04T00:00:00+00:00 List-Id: In article , Robert A Duff wrote: >Well, the goal is to make sure that the compiler can *check* that the >abstract value of an 'in' parameter is not modified. And any time you >want to check things at compile time, you have to put up with rules that >are more pessimistic than they might be. In this case, the compiler >knows nothing of you "abstract" values. The language therefore requires >it to check that the concrete values are not modified. > >The alternative would be for 'in' mode to just be a comment in the code, >and the compiler wouldn't check anything. Then you could modify the >concrete value while making sure the abstract value is not modified. >But that would obviously be error prone. > >I don't see any way around this. I don't think there is an easy solution. In RESOLVE the behavior of the operation would be formally specified. The requirement that the abstract value of an 'in' mode (RESOLVE's 'preserves' mode in this case) parameter not change becomes a proof obligation. I understand why Ada takes the conservative approach. However, this approach seems to force unnecessary copying of objects and forces the programmer to reason about the code at a less abstract level. >Consider: > > X: constant Integer := 1; > ... > Y: Integer := Read_Data_From_Input_File; > X := Y; -- Illegal! > >Should the above be legal? After all, if the programmer ensures that Y >is 1, then there's no harm done. You wouldn't want to allow this, but what if X were an 'in' mode formal parameter? Then code similar to this would generate a proof obligation that could not be satisfied. As long as some form of verification process is applied faithfully, allowing 'in' mode parameters to be changed should not be a problem. >Consider: > > Do_Something("string literal"); > >If Do_Something is allowed to modify the concrete value of its "in"-mode >parameter, what is the compiler supposed to do with the result? Literal values would require some special handling in an "all objects" framework. I think there are several different strategies that could be used. Upon elaboration of the unit containing the string literal (and perhaps multiple references to it), a single object could be set up with the literal as its value. The above call could then be implemented as a call passing in a String object, not a string value. The string object could be manipulated, but Do_Something would be required, as above, to return with the object's value unaltered. I doubt many current Ada compilers are likely to take this approach :-). Dave dgibson@cis.ohio-state.edu