Re: Ada 2012: In-out parameters for functions

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Tue, 07 May 2013 05:59:49 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
>
>      -- SPARK way to solve the issue
>      -- and to make explicit what it do.

To not count side effects, which are not even visible in any way at the  
sub‑program declaration, so not even declared out/in–out to expect with  
these. Except for SPARK (the same as above with an added side effect with  
read/write involving a global variable):


     E : U; -- Side effect with this.

     procedure P
       (A :    out T;
        B : in out T;
        C : in     T);
     --# global E;
     --# derives
     --#    A from B, C, E &
     --#    B from B, C &
     --#    E from B;


Here, `E` appears at the declaration of `P` and is like declared in‑out  
(`A` derived from `E` means like if it was`in` and `E` derived from `B`  
means like if it was also `out`).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University