Re: High-Integrity OO and controlled types

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 04.05.11 18:23, Dmitry A. Kazakov wrote:

>> Try adding pragma Profile (Ravenscar) there ;.)
> 
> I don't care much about Ravenscar, which is too limiting for almost
> anything. There are limitations to make life easier for the readers and
> ones for the compiler and prover. They are not same, some contradict to the
> goals of each other. I always choose the former over the latter.

Does it work when systems need to be fast at the lower levels?

>> Is there really little overhead when Restore is replaced
>> with some objects?
> 
> [...]
> 
> Negligible since used upon an exception, which I hope is not to propagate
> at 100ns rate.

Ah, o.K., I should have said source code maintenance overhead, too,
and increased system complexity.  The program now uses nesting, a language
feature. In order to go with types for the same effects, it will have to be
transformed. To replace the Restore procedure, the transformation
would have to add not just objects but also "indirections" that
make up for the effects.  I think that what you said earlier?
If this is the case, then I wonder whether or not this kind of
overhead is worth the effort.

All of this does not address the issue of how to hook "nested rollback".