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=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI autolearn=unavailable autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,fe9ec916c5bbbd59,start X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-12-11 11:07:04 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!newsfeeds.belnet.be!news.belnet.be!opentransit.net!wanadoo.fr!freenix!enst!enst.fr!not-for-mail From: "Alexandre E. Kopilovitch" Newsgroups: comp.lang.ada Subject: Consider her way -- Re: Dimensionality Checking Date: Tue, 11 Dec 2001 22:10:48 +0300 (MSK) Organization: ENST, France Sender: comp.lang.ada-admin@ada.eu.org Message-ID: Reply-To: comp.lang.ada@ada.eu.org NNTP-Posting-Host: marvin.enst.fr Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: avanie.enst.fr 1008097622 87257 137.194.161.2 (11 Dec 2001 19:07:02 GMT) X-Complaints-To: usenet@enst.fr NNTP-Posting-Date: Tue, 11 Dec 2001 19:07:02 +0000 (UTC) To: comp.lang.ada@ada.eu.org Return-Path: X-Mailer: Mail/@ [v2.44 MSDOS] Errors-To: comp.lang.ada-admin@ada.eu.org X-BeenThere: comp.lang.ada@ada.eu.org X-Mailman-Version: 2.0.6 Precedence: bulk List-Help: List-Post: List-Subscribe: , List-Id: comp.lang.ada mail<->news gateway List-Unsubscribe: , Errors-To: comp.lang.ada-admin@ada.eu.org X-BeenThere: comp.lang.ada@ada.eu.org Xref: archiver1.google.com comp.lang.ada:17780 Date: 2001-12-11T22:10:48+03:00 Recent discussion about the dimensions/unit analysis seems to me... well, not directed by the spirit of the Ada language. As far as I understand, all participants of the discussion presume that if the dimensional/unit analysis should be done for an Ada program then it must be performed entirely with the facilities of Ada language itself. I think that that assumption is plain wrong. Let us consider what the dimensional/unit analysis is, in general terms. For every dimension/unit U we have the mapping Deg_U, which assigns the rational numbers to the subtypes (that is, the domain of the Deg_U is the set of all subtypes in our Ada program, and the range of the Deg_U is the set of rational numbers). We extend this mapping to the variables and user-defined functions, using the subtype of a variable and the subtype that a function returns. The mapping Deg_U is "logarithmic", that is, for any variables (or user-defined functions) X, Y, Z: Z is compatible with X * Y implies Deg_U(Z) = Deg_U(X) + Deg_U(Y), and Z is compatible with X / Y implies Deg_U(Z) = Deg_U(X) - Deg_U(Y), Then we require for all assignments (including an argument passing), additions and subtractions in our program, that the values of the mapping Deg_U for the right operand (side) must be equal to the corresponding value for the left operand. This requirement permits us to define Deg_U over the rational expressions. Taking into account that the "logarithmic" rule effectively determines the values of the mapping for the square root, we conclude that the mapping Deg_U is defined over the algebraic expressions. The final step is to assign zero value to all standard (predefined) transcendent functions (such as Sin etc.). So, the mapping Deg_U is defined for all expressions, and the condition to be verified is already formulated: for each assignment, addition and subtraction the value of the mapping Deg_U on the right operand must be equal to the corresponding value on the left operand. This is a definition of the basic "linear" dimensional analysis. One may construct other, more sophisticated forms of the dimensional analysis for the specific purposes. Now let's recall the fact that the Ada is not a problem-oriented language, but rather a "superassembler". It intentionally and carefully avoids all paradigms that aren't closely related to the real computer architectures or to the general software engineering, even if those paradigms are heavily used in some significant application area. (Note that I'm speaking here about the paradigms; the data representation issues are another matter, that is a natural job for an assembler.) Obviously, the dimensionality paradigm is one of the kind that Ada avoids: it belongs neither to a computer architecture nor to the general software engineering, but to the particular application area, no matter how significant it is in the real world. Therefore Ada most probably will not take any move to support it directly. The proper way to do the dimensional/unit analysis for the Ada programs is to use the ASIS and some suitable language processor, I guess that the SML might be the best for this purpose (because it is well-suited for the manipulations with the algebraic type systems). So the configuration of the whole tool chain may look like that: dimension/unit values for the subtypes | | \|/ | |------| |---------| |-------------| | ASIS | ------> | SML | ------ | SML | | tool | | program | | interpreter | |------| |---------| |-------------| | | /|\ | | \|/ | | |----------| diagnostic output | Ada | | compiler | |----------| | /|\ | | program to be verified Finally, I'll try to explain why the subtypes, and not the types, are the natural carriers for the dimensionality info. Briefly, with the physical magnitudes, all the dimensionalities are imaginary, and only the repetition count within some underlying measurement process is real. That count is obviously dimensionless. In fact, a dimension of physical magnitude is the abstraction for the class of the instruments with which we can measure the magnitude. If you do not like such vague metaphysical arguments then consider the following question: if X and X*X belong to the different types, how will you treat (interpret) the usual approximations by the Taylor series? And as for the units, I hope everyone will agree that there is no fundamental difference (in physics) between miles and kilometers. Alexander Kopilovitch aek@vib.usr.pu.ru Saint-Petersburg Russia