Re: ANN: New technical paper from Ada Europe 2004 now available

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Hyman Rosen wrote:
> Mike Silva wrote:
> 
>> Isn't it really straining to complain about the style (not
>> correctness, but style) of automatically generated code?
> 
> 
> No. One of the claims of the paper is that the generated C
> code is readable and maintainable in and of itself; indeed
> that is one of the main points of the paper.
> 

I don't recall making this claim.  I said that the translation process 
is "transparent and traceable" and that the C provides a useful 
intermediate representation for object code verification purposes.  I 
think these statement stand.

We certainly wouldn't recommend modification of the C because that 
immediately throws away all the verification benefits that have been 
gain by analysing the intermediate SPARK model.

It is probably true that the C /could/ be maintained if, for example, 
the translation or SPARK parts of the tool chain were suddenly to become 
unavailable.

Peter