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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,48e1a3c594fb62e8
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news2.google.com!news2.google.com!npeer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!nx02.iad01.newshosting.com!newshosting.com!novia!news-out.readnews.com!postnews3.readnews.com!not-for-mail
Message-Id: <4bee9bea$0$2405$4d3efbfe@news.sover.net>
From: "Peter C. Chapin" <pcc482719@gmail.com>
Subject: Re: SPARK
Newsgroups: comp.lang.ada
Date: Sat, 15 May 2010 09:09:08 -0400
References: <op.vcl6900wule2fv@garhos> <op.vcmiwxowule2fv@garhos>
 <Pine.LNX.4.64.1005131108120.27720@medsec1.medien.uni-weimar.de>
 <op.vcnkzltoule2fv@garhos>
User-Agent: KNode/0.10.9
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8Bit
Organization: SoVerNet (sover.net)
NNTP-Posting-Host: 2d62768b.news.sover.net
X-Trace: 
 DXC=VhbQIP05[fg>7Djcl\Km1iK6_LM2JZB_cc>ZAR<SWjMe:WUUlR<856o9a^?UjZ<C\hUeMO<;LMKJo
X-Complaints-To: abuse@sover.net
Xref: g2news2.google.com comp.lang.ada:11636
Date: 2010-05-15T09:09:08-04:00
List-Id: <comp.lang.ada>

Yannick Duchêne (Hibou57) wrote:

>>
>>   f(g(I) + f(f(g(I)))**2,
>>
>> or to
>>
>>   f(f(g(I))) + f(g(I))**2.
> A function optimized (which save computing of already computed inputs)  
> using memoisation, does not exposes this behavior.

If it works properly, yes, but what if it doesn't?

> How to make it formal : may be giving the proof the function is the only  
> one to access memoisation storage between function invokation, so, that  
> this data are mechanically private to the function. Then, demonstrate  
> there is two paths to the result : one which is the basic computation and  
> one which retrieve the result of a similar previous computation. This  
> latter step could rely on the computation of a key to access this data.  
> Then demonstrate that for a given input, the computed key is always the  
> same (input <-> key association). Now, the hard part may be to demonstrate  
> the key is used to access the result which was computed previously for the  
> same input that the one which was used to compute the key.
> 
> Obviously, the function should be the only one to access this data.
> 
> There is a concept in SPARK, the one of variable package and  
> state-machines. May be there could be some room for a concept which could  
> be something like function-package ?

While this might be possible, it does sound rather complicated. I can see why
SPARK doesn't currently go down this path.

Peter