Ada: Using a private variable in a precondition of a public function

user_7416891 0
Viewed 203

The following is an attempt to produce my problem with the minimum code (it is not intended to be a useful program).

My problem is that I want to make a precondition on a public function dependent on a private variable. I have to declare my function before the "private" indicator and my variables after that indicator. This means that I get the compilation error

problem.ads:10:16: "secondPrivateVariable" is undefined problem.ads:10:40: "firstPrivateVariable" is undefined

I have tried putting placeholder definitions above the function, but then I get compilation errors about conflicting definitions.

package Problem is
pragma Elaborate_Body (Problem);

    function publicAPI(which : Positive) return Natural with
        Pre => secondPrivateVariable > firstPrivateVariable;
    --  should only be called when second > first

private
    --  the following variables are used by many procedures and
    --  should be kept private

    firstPrivateVariable : Natural := 7;
    secondPrivateVariable : Natural := 465;

end Problem;

Any assistance would be welcomed.

ada
1 Answers

You could wrap the check in a function:

   function Call_Permitted return Boolean;

   function publicAPI(which : Positive) return Natural with
     Pre => Call_Permitted;

private

   firstPrivateVariable : Natural := 7;
   secondPrivateVariable : Natural := 465;

   function Call_Permitted return Boolean is
     (secondPrivateVariable > FirstPrivateVariable);

If Call_Permitted is only to be used locally and only to generate object code if assertions are enabled, you could say

   function Call_Permitted return Boolean with Ghost;

(this is a SPARK-related feature, probably only available in GNAT)

user_408510
Related