Re: Ada style of passing 'in' parameters considered dangerous?

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

Antti Sykari <jsykari@gamma.hut.fi> wrote in message news:<86isvuzabx.fsf@hoastest1-8c.hoasnet.inet.fi>...
> - If there are such cases, could it have been prevented by having
>   different policy in the language?

Yes - use SPARK!

>   Do you think it would've been
>   better to force the programmer to specify the parameter passing
>   mechanism, for example?

How?  Forcing programmers to explicitly use access parameters,
for instance, sounds like a really bad idea.

SPARK is free from parameter passing dependencies.  The language
doesn't specify a mechanism (this would be a big mistake, since
the language wouldn't then be a true subset of Ada...), but rather
simply enforces language rules so that it is impossible to write a program
where the mechanism chosen by a compiler can ever result in differing
dynamic semantics at run-time.  These rules are checked by the Examiner.
All violations are detected statically (in polynomial time) for incomplete
programs (basically meaning the rules are chekcable only using
the specification of called units, not their bodies...very important
for doing analysis when you haven't actually finished
writing the program yet!)
 - Rod, SPARK Team