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.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,5aa1f17e1cbe0afb
X-Google-Attributes: gid103376,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news1.google.com!postnews.google.com!e67g2000hsa.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: Re: SPARK and static unit checking?
Date: Mon, 14 Apr 2008 07:57:49 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <87c37b48-d523-4d13-b10e-474cda527753@e67g2000hsa.googlegroups.com>
References: 
 <af9b42f7-b24c-4ca5-8a49-1ea9c15e1f37@y21g2000hsf.googlegroups.com>
	<O1nEKjD2FmAIJwBH@diphi.demon.co.uk>
 <f6625d23-9ff0-417d-9d87-890cf52ec045@a22g2000hsc.googlegroups.com>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1208185069 19285 127.0.0.1 (14 Apr 2008 14:57:49
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 14 Apr 2008 14:57:49 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: e67g2000hsa.googlegroups.com; posting-host=217.205.167.137;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.8.1.13)
	Gecko/20080311 Firefox/2.0.0.13,gzip(gfe),gzip(gfe)
X-HTTP-Via: 1.1 bloxx:3128 (squid/2.5.STABLE11)
Xref: g2news1.google.com comp.lang.ada:20934
Date: 2008-04-14T07:57:49-07:00
List-Id: <comp.lang.ada>

SPARK has a few general princles regarding the arithmetic
operators.

1) They are always "monotonic" meaning they take and return the same
type - the binary operators, for example, always have the signature
  (Left, Right : in T) return T

2) There is no re-declaration, renaming, or user-defined overloading
of the
operators, so "+" _always_ means "arithmetic addition" (which might
be signed integer, modular integer, floating, or fixed, of course...)

3) You can't change the base-name of an operator via a renaming,
which,
as Bob Duff pointed out in another thread, is a dreadful thing to do
anyway.

You can define functions with identifiers for names if you can put
up with having to write "My_Plus (A, B)" instead of "A + B" for
instance.

- Rod Chapman, SPARK Team