Ada：在公共函数的前提下使用私有变量

Question

以下是尝试用最少的代码产生我的问题（它不是一个有用的程序）。

我的问题是我想对依赖于私有变量的公共函数做一个先决条件。我必须在“私有”指标之前声明我的函数，并在该指标之后声明我的变量。这意味着我收到编译错误

question.ads:10:16: "secondPrivateVariable" 未定义问题.ads:10:40: "firstPrivateVariable" 未定义

我曾尝试将占位符定义放在函数上方，但随后出现有关定义冲突的编译错误。

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;

欢迎任何帮助。

Answer 1

您可以将支票包装在一个函数中：

   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);

如果Call_Permitted仅在本地使用并且仅在启用断言时生成目标代码，您可以说

   function Call_Permitted return Boolean with Ghost;

（这是一个 SPARK 相关的特性，可能只在 GNAT 中可用）