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 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,2078ce7aac45af5b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.224.219.144 with SMTP id hu16mr3501703qab.1.1353089418219;
        Fri, 16 Nov 2012 10:10:18 -0800 (PST)
Received: by 10.49.71.6 with SMTP id q6mr1150281qeu.10.1353089418195; Fri, 16
 Nov 2012 10:10:18 -0800 (PST)
Path: 
 gf5ni327qab.0!nntp.google.com!u2no2811959qal.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 16 Nov 2012 10:10:18 -0800 (PST)
In-Reply-To: <aPOdnc5Ki_61rjvNRVn_vwA@giganews.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=92.235.245.78;
 posting-account=g4n69woAAACHKbpceNrvOhHWViIbdQ9G
NNTP-Posting-Host: 92.235.245.78
References: <0114d327-9f9f-4ad2-9281-56331d11a90c@googlegroups.com>
 <e33b09e3-7840-42d0-886b-8cf1ec7bf9d3@googlegroups.com>
 <15w6caje3zsh$.t5nqtwoa77x5$.dlg@40tude.net>
 <NLWdnUlRH6U-kjjN4p2dnAA@giganews.com>
 <r00q8we9dpjp.1410izlwuflo3$.dlg@40tude.net>
 <WdGdnd-Z6-nFHzjN4p2dnAA@giganews.com> <k84lbn$95o$1@munin.nbi.dk>
 <aPOdnc5Ki_61rjvNRVn_vwA@giganews.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <52b2eaf5-70c0-42c7-96ee-944917d642e0@googlegroups.com>
Subject: Re: Ada202X : Adding functors
From: Martin <martin@thedowies.com>
Injection-Date: Fri, 16 Nov 2012 18:10:18 +0000
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-11-16T10:10:18-08:00
List-Id: <comp.lang.ada>

On Friday, November 16, 2012 12:35:52 PM UTC, Peter C. Chapin wrote:
> On 11/16/2012 01:09 AM, Randy Brukardt wrote:
> 
> 
> 
> > There's more to a function contract than just the type-and-result-profile!
> 
> > To truly statically check such things, you also have to match the
> 
> > precondition, the postcondition, the exception contract, the global in/out
> 
> > usage, and so on. (Matching doesn't necessarily mean exact equivalence, of
> 
> > course, which makes it even harder.)
> 
> 
> 
> I should probably first make it clear that I'm not necessarily 
> 
> advocating for the addition of lambda expressions to Ada. My posts in 
> 
> this thread are only to say that lambda expressions are not necessarily 
> 
> any more weakly typed than any other kind of expression (as Dmitry asserts).
> 
> 
> 
> Anyway, it is certainly true that the contract extends beyond the 
> 
> type-and-result-profile. In that respect a function type is a richer 
> 
> entity than, say, type Integer... of course. Yet one could imagine a 
> 
> hypothetical language in which some of this additional richness was 
> 
> packed into the function type either with appropriate syntax or some 
> 
> sort of extra-linguistic annotations. In that case, parameters of higher 
> 
> order subprograms could declare this additional information, making it 
> 
> available for static analysis.
> 
> 
> 
> The full contract of a function includes its semantics as well. It would 
> 
> be interesting to speculate on what it would take to describe the 
> 
> semantics of a function with some suitable formal notation and decorate 
> 
> declarations with that information for purposes of static analysis. For 
> 
> example:
> 
> 
> 
> procedure Process_With(X : Integer,
> 
>                         F : Some_Function_Type with Semantics => (
> 
>    -- Semantics of required function written in Z (for example)
> 
>    )) is
> 
> begin
> 
>    -- etc...
> 
> end Process_With;

Couldn't we just re-use what Ada already provides? Isn't it pre/post conditions?

procedure Process_With (X : Integer;
                                      F : Some_Function_Type
                                         with Pre => X > 10 and Post <= Some_Function_Type'Return > 100) is
begin
...
end Process_With;

-- Martin