I tried something new for my Assertion library. To be precice this:
---
-- Assert that a discrete value is equal a given value
--
--: @param Actual Actual value
--: @param Expected Expected value
--: @param Name Name of variable or function restlt.
--: @param Source Source code
--: @param Line Line number
--: @exception System.Assertions.Assert_Failure Condition not meet
procedure Equal
(Actual : Discrete_Type;
Expected : Discrete_Type;
Name : String;
Source : String := GNAT.Source_Info.File;
Line : Natural := GNAT.Source_Info.Line) with
Post => Actual = Expected;
This results in and “postcondition does not check the outcome of calling” warning. Which is true but also the condition will be true at the end of the function because the function with throw an exception otherwise.
Shouldn’t Actual be an out value? Otherwise, the procedure (as declared in the Postcondition) is just making sure that the two input values are the same.
Anyhow, I believe that you need to use Actual'Result in order to tell SPARK that what you are checking is the resulting value of Actual as computed by the procedure and not the input value as it comes. That way, SPARK knows that it actually has to run the computation of Equal rather than just analyzing the inputs as they come. Otherwise, what you are writing could be a Pre and it would be the exact same, which is not what you want.
Postconditions are for the effect of your subprogram on its outputs. As your procedure has no outputs, it can have no meaningful postcondition. Sounds like what you want is a precondition:
procedure Equal (Actual : in Discrete_Type;
Expected : in Discrete_Type;
Name : in String;
Source : in String := GNAT.Source_Info.File;
Line : in Natural := GNAT.Source_Info.Line)
is null with
Pre => Actual = Expected or else
raise System.Assertions.Assert_Failure with
Name & ' ' & Source & Line'Image;
procedure Equal
(Actual : Discrete_Type;
Expected : Discrete_Type;
Name : String;
Source : String := GNAT.Source_Info.File;
Line : Natural := GNAT.Source_Info.Line)
is
begin
if not (Actual = Expected) then
Report_Assertion
(Message => "Discrete_Type «" & Name & "» " & Actual'Image & " is not equal to " & Expected'Image,
Source => Source,
Line => Line);
end if;
end Equal;
When the procedure return the values are the same — or the procedure doesn’t return.
Interesting. How will the system react when the contracts are checked vs when contracts are not checked?
This is true.
(Well, there could be context-bound or global objects.)
No, precondition is wrong here: preconditions are the things that must be true for calling the function. Your usage has an if conditioning on this, and so this is implying that the thing you’re using as a precondition is not always true, and therefore should not be a precondition.
Looking at the naming, and the structure, it is obvious that you’re building an assertion-system; there’s really two considerations here: (1) is this for what is implementing an external environment, like, say, you’re building a compiler; and (2) is this for integrating with some already extant system, say, a template parser? — Think on the implications of these two forms.
In general, for #1 —that is, where the “error conditions” of “bad syntax” (i.e. unexpected token)— preconditions and postconditions are the wrong tool: because you have to deal with the error before you have something valid to pass to the next stage of processing. You can, however, use postconditions to assert that the thing provided by the previous stage is valid, and postconditions assuring that a result from this state meets some particular quality (which can be all-/part-of the next stage’s precondition).
TL;DR — This:
(IIRC, in SPARK you can use exceptions, so long as they are handled in-scope.)
Function Operation( Input : Stage_1_Data ) return Stage_2_Data is
Begin
--… extract info from Stage_1
if not Expected( Quality_1(Input), Some_Value ) then
Raise Unexpected with "Description of fault.";
end if;
--… construct info for Stage_2
Return Result : Stage_2_Data do
if not Expected( Quality_A(Result), Some_Value ) then
Raise Unexpected with "Description of fault.";
end if;
End return;
End Operation;
OR
(Because we don’t have unhandled exceptions in SPARK.)
Use some Error-condition record.
It’s already finished, working and used in almost all my crates. I’m looking for potential improvements.
Neither but closer to 2. It’s for unit testing. When the condition is not meet an exception is raised and then caught by AUnit which will will then continue with the next test and print out an test at the end the test run.
As such having contracts are merely a reassurance that the condition is satisfied. As I said initially I’m just experimenting on how far I can push contracts.
Yes, that is probably the case, so I won’t be adding them.
I’m not using SPARK to test prove the code. I don’t do embedded applications. The contracts are checked at runtime as part of the unit tests. It was only an experiment to see what else can be done.
„Doesn’t work“ is a valid result of an experiment .
so the effect of turning assertion checking on or off will be the same. Since I’ve now seen your body, it appears you want to check the condition regardless of the state of assertion checking. You could use
pragma Assertion_Policy (Check);
to force it on for your unit containing Equal, or, since you use this for testing, simply ensure that you compile your tests with it on (-gnata, since you’re using GNAT). Or you can accept that pre- and postconditions don’t really meet your needs and rely on comments to document this.
.