Re: Why .ads as well as .adb?

[joakimds@kth.se]

Den söndag 2 juni 2019 kl. 02:48:18 UTC+2 skrev John Perry:
> Hello
> 
> I understand that Ada, like Modula-2 and Modula-3, and arguably like C++, requires a definition file (.ads) as well as an implementation file (.adb). With Oberon, Wirth moved away from definition files, using a symbol to indicate which module identifiers should be exported. (Someone else may have done this before him; it's just that I'm most familiar with this history.) Most languages I'm familiar with these days do something similar, either via public/private or some other mechanism.
> 
> As far as I can tell, though, Ada has stuck with the two separate files, rather than, say, generating an .ads from an .adb with export markup.
> 
> Is there a reason Ada hasn't moved to this simpler structure?
> 
> john perry

Expanding on what Dmitry wrote it is not possible to generate specifications from the implementation. Consider for example a simple function that takes an integer as input and multiplies with 10 and then returns the result:

function Multiply_By_10 (I : Integer) return Integer is
begin
   return 10*I;
end Multiply_By_10;

One might think that the specification/declaration of this function is merely

function Multiply_By_10 (I : Integer) return Integer;

but with contract-based programming it is possible to specify that the contract for the integer argument must be a number between 1 and 10 and the result must be a number between 10 and 100.

function Multiply_By_10 (I : Integer) return Integer with
   Pre  => I >= 1 and I <= 10,
   Post => Multiply_By_10'Result >= 10 and Multiply_By_10'Result <= 100;

The pre- and post-conditions may be important for static code analysis tools to prove/verify that an application is correctly implemented. Note that the information needed to specify the pre- and post-conditions are missing in the implementation. One could perhaps auto-generate pre- and post-conditions from the body but it will probably not correspond to what the developer wishes to set up as a contract for the subprogram. From my experience, the specification of contracts can be many, many lines of code. To be able to cleanly separate the contracts from the implementations is very useful and convenient.