艾达：在公共功能的前提下使用私有变量

问题描述

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

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

problem.ads:10:16：“ secondPrivateVariable”未定义 problem.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;

任何帮助都将受到欢迎。

解决方法

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

   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中可用）