[gclist] Finalization, again

[Fergus Henderson]

On 06-Oct-2001, David Chase <chase@world.std.com> wrote:
> At 12:09 PM 10/5/2001 +0100, Nick Barnes wrote:
> >Proof-carrying code, Necula et al, addresses exactly this sort of
> >point.  You need to know that some code (e.g. a downloaded applet) has
> >certain properties (runs in a given amount of time, doesn't perform
> >"illegal" accesses, doesn't raise exceptions).  So you require that
> >the code should come with a proof of these properties.  You can check
> >the proof in a small finite time.  Generating such a proof is very
> >much harder(!).
> 
> How hard is it?  (I suppose there's papers I should read.)

Here's one that may be relevant:

     * Termination analysis for Mercury.
       Chris Speirs, Zoltan Somogyi and Harald Sondergaard.
       Proceedings of the Fourth Static Analysis Symposium , Paris,
       France, September 1997, pages 157-171.
       Available from <http://www.cs.mu.oz.au/mercury/information/papers.html>.

       This paper presents the algorithms of the Mercury termination
       analyser, discusses how real-world aspects of the language such as
       modules, higher-order features, foreign language code, and
       declarative input/output can be handled, and evaluates the
       performance of the analyser both on a set of standard test
       programs and on the Mercury compiler itself.

Work on this topic is continuing, with Zoltan Somogyi having recently
been successful in applying for an Australian Research Council grant
involving work on automatic complexity analysis of Mercury programs.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.