[Grace-core] Minutes of Teleconference 23-24.8.12

James Noble kjx at ecs.vuw.ac.nz
Mon Aug 27 01:09:29 PDT 2012


Bart (& all)

On 24/08/2012, at 22:05 PM, Bart Jacobs wrote:

> Aha, exceptions! I've been looking at exception handling for my program verification research. It turns out that the classical exception handling mechanism (which is used by most programming languages) leads to some verification issues. 

that reminds me that we should look at other aspects of the language design which may help (or hinder) verification.

The only obvious one I can think of is named result variables - Pascal had a named variable that is returned,
so post-conditions can name that variable - I think Eiffel does something similar?  Go is bringing back names
for return values, too.

But I'm sure there must be others!

James


More information about the Grace-core mailing list