SPARK 2014 Rationale: Information Flow
by Florian Schanda –
We will start off with a simple example. Lets assume that we want to write a procedure that doubles and then swaps variables X and Y. The final value of X should depend only on the original value of Y and the final value of Y should depend only on the original value of X. So now let's write some code and add the depends contract that we just mentioned on it.
procedure Double_And_SWAP (X, Y : in out Integer)
with Global => null, -- We use no global variables.
Depends => (X => Y, -- This reads as: "X depends on Y"
Y => X) -- This reads as: "Y depends on X"
is
Tmp : Integer;
begin
X := X * 2;
Y := Y * 2;
Tmp := X;
X := Y;
X := Tmp; -- Oops, I mistyped... (should be "Y := Tmp;")
end Double_And_SWAP;When the tools analyze the above code, they complain that the depends annotation does not match the implementation. Both variables depend on themselves instead of each other. At this point, to make the error go away we have to either change the code, or change the dependency relation. In this particular example the problem lies with the code. However, this might not always be the case, it could very well be that our contracts/specifications were actually wrong because we failed to notice a dependency and consequently failed to capture it on the Depends aspect. Had we not added the dependency relation, it would have been easy to miss the typo and end up with an error in our code. Spotting the error was easy on this occasion but the more complicated the code the harder it gets. The tools make our life easier by highlighting the path in the code that leads to the discrepancy.
The "Plan first, act later!" advice, seems to be applicable here since programmers should first formulate their Dependency relations and then proceed to the implementation.
Lets now point out some key characteristics of aspect Depends. The Depends aspect tells us how the outputs of a subprogram relate to the inputs. Inputs always remain unchanged, so they cannot depend on anything. If an output 'X' does not depend on any input, then we have to explicitly state this by writing "Depends => (X => null)". Similarly, if an input 'Y' of the subprogram is not used by any output, we have to state this by writing "Depends => (null => Y)".
Suppose that we want to write a procedure that takes a single parameter 'Y' and then sleeps for 'Y' milliseconds. Since time is not modelled in SPARK, this procedure will appear to have no output and input 'Y' will appear to be doing nothing. The dependency relation of this Sleep procedure will look exactly as mentioned before "Depends => (null => Y)".
Lets now try to do the inverse. We will look at an unannotated piece of code and try to figure out what the corresponding Depends aspect should have been.
procedure No_Depends is
begin
if Condition then
X := Y;
end if;
end No_Depends;So let me think out loud... Since global variable Condition and global variable Y are only being read, they are inputs. Global variable X on the other hand is only ever written, so it has to just be an output. So the first Dependency relation that pops into mind is "Depends => (X => (Y, Condition))". Right?
...
WRONG ! When Condition is False, X remains exactly the way it was. So X depends on itself and is in fact also an input. It is as if we had written:
procedure No_Depends is
begin
if Condition then
X := Y;
else
X := X;
end if;
end No_Depends;The correct dependency for the code above would be "Depends => (X => (X, Y, Condition))". A shorthand for this is "Depends => (X =>+ (Y, Condition))". The '+' symbol means that variables on the left hand side also depend on themselves. So, the thing to remember here is that even though calculating the dependency relation of a subprogram is not too hard, there are some subtleties involved.
Aspect Depends tells us how the outputs of a subprogram relate to its inputs. This improves readability and maintainability of the code by strengthening the interface specification of a subprogram. In certain contexts, such as the development of secure systems, this is a very powerful verification/assurance technique. Here, it is recommended that programmers provide dependency relations before they start writing the actual code so that the tools can verify the validity of the implementation against the annotations. If we all were to adopt this habit, higher quality code would be generated and the world would be a better and more secure place! :D