Re: Rust's temporal safety for Ada/SPARK

["Jeffrey R. Carter" <spam.jrcarter.not@spam.not.acm.org>]

On 05/15/2017 09:07 PM, Simon Wright wrote:
>
> I was thinking that an alternative subject area might be code like
>
>       procedure Add (Dest : in out Integer; N : Integer)
>         with
>           Post => Dest = Dest'Old + N;
>
>       procedure Add (Dest : in out Integer; N : Integer)
>       is
>       begin
>          Dest := Dest + N;
>       end Add;
>
>       Dest : Integer := 42;
>
>    ...
>
>       Add (Dest, Dest);
>
> (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?).

Elementary types are passed by copy, so you don't have any paths to the variable 
Dest inside Add. That's why this is OK. If the type might be by reference, 
though, this can be a problem.

-- 
Jeff Carter
"Strange women lying in ponds distributing swords
is no basis for a system of government."
Monty Python & the Holy Grail
66