1. Please can you tell me whether or not the parameters (in or out or in out) and the depends clause, are correct for the rest of the program.

2. Question: I am unsure if the loop invariant can 'use' a parameter in order to make it an in parameter (or initialise one to make it an out).

For example if this line was missing Aux : Integer := X; would x be made an in parameter here:

Loop Invariant (Z = X + Aux - Y) ?

Also does Z depend on X because of the loop invariant? I am just unsure if the loop invariant works like pre and post conditions or if it is actually part of the program where parameters can be used etc..

Here is the ads file:

pragma SPARK MODE;
procedure Myproc (X : in Integer; Y : in Integer; Z : out Integer)
with Depends => (Z => (Y,Z)),
     Post => (Z = X - Y);

here is the adb file:

pragma SPARK MODE;
procedure Myproc (X : in Integer; Y : in Integer; Z : out Integer) is
    Aux : Integer := X;
begin
    Z := Y;
    loop
        pragma Loop Invariant (Z = X + Aux - Y);
        exit when Aux = 0;
        Aux := Aux - 1;
        Z := Z - 2;
    end loop;
end Myproc;

I tried in Gnat studio and am now unsure