CODEWITHSUNDEEP
ada
Chris Hobbs
Chris Hobbs

Reputation: 445

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

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.

Upvotes: 3

Views: 390

Answers (1)

Simon Wright
Simon Wright

Reputation: 25491

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)

Upvotes: 7

Related Questions