Re: Rust's temporal safety for Ada/SPARK

[moy@adacore.com]

On Monday, May 15, 2017 at 9:07:49 PM UTC+2, Simon Wright wrote:
> (where we have alternate paths to the variable Dest); but SPARK is happy
> and the runtime check isn't triggered, so I suppose the ARM supports
> this (by copy-out?).

Hi Simon, SPARK is happy because there is no problematic aliasing with the code you posted. Since N is of scalar type, it is always passed by copy. Since N is also of mode 'in', it is only copied on entry, not copied back. So the contract you wrote on Add is still valid even if you call it on Dest and Dest. But the postcondition only holds upon returning from Add, not after the call statement. Between these two, the value returned in parameter Dest is copied back in local variable Dest. This is how both the GNAT compiler and the GNATprove analyzer understand it.

> Still, the usage shouldn't pass code review, I think.

I guess it depends on the meaning of the code. If the use of the same value in different parameters is confusing, indeed not. Otherwise, there is nothing wrong with that code.