Предварительные условия Ada, которые используют частные функции?

Question

Я очень новичок в Ada, я действительно смущен тем, что делаю вещи частями в файле спецификации Ada. У меня есть несколько частных функций, которые должны оставаться закрытыми, но я хочу использовать их как часть условий до и после некоторых моих не-частных процедур. Когда я пытаюсь найти их, он говорит, что функция не определена?

Я думал, что создание функции private означает, что доступно только для вызова внутри этого пакета? т.е. как .ad, так и .adb-файл?

Ниже приведен мой код. Таким образом, мои условия pre/post моей процедуры Lift_Nozzle используют частные функции Get_Active_Pump и Get_Pump, но когда я проверяю семантику, это говорит о том, что они не определены (потому что они являются частными?). Есть ли для этого работа? Благодаря

pump_unit.ads (некоторые из них):

with Pumps; use Pumps; 
with Shared_Types; use Shared_Types; 

package Pump_Unit is 

    procedure Lift_Nozzle(x: Shared_Types.ID_Value) 
    with Pre => Get_Active_Pump = 0 and then 
    Get_Pump(x).State = base, 
    Post => Get_Pump(x).State = ready and then 
    Get_Active_Pump = x; 

private 

    type Private_Pumps is array (Integer range 1..3) of Pumps.Pump; 
    function Get_Pump(x: Shared_Types.ID_Value) return Pumps.Pump; 
    function Get_Active_Pump return Shared_Types.ID_Value; 

end Pump_Unit; 

pump_unit.abd (некоторые из них):

with Pumps; 
with Shared_Types; 

package body Pump_Unit is 

    Pump_Array: Private_Pumps; 

    --ID of the current pump being used at the pump unit. 0=no pump currently in use. 
    Active_Pump: Shared_Types.ID_Value; 

    function Get_Active_Pump return Shared_Types.ID_Value is 
    begin -- Get_Active_Pump 
     return Active_Pump; 
    end Get_Active_Pump; 

    function Get_Pump(x: Shared_Types.ID_Value) return Pumps.Pump is 
     use type Shared_Types.ID_Value; 
    begin -- Get_Pump 
     for Index in 1..3 loop 
     if Pump_Array(Index).ID = x then 
      return Pump_Array(Index); 
     end if; 
     end loop; 
     return Pump_Array(1); 
    end Get_Pump; 

    procedure Lift_Nozzle(x: Shared_Types.ID_Value) is 
     use type Shared_Types.ID_Value; 
     pump : Pumps.Pump; 
    begin -- Lift_Nozzle 
     pump := Get_Pump(x); 
     pump.State := Pumps.ready; 
     Active_Pump := x; 
    end Lift_Nozzle; 

begin 

    Pump_Array := 
    ((ID => 1, Fuel_Variety => Pumps.Fuel_91, State => Pumps.base, Price => 1.70, Reservoir => 50000, Active => False), 
     (ID => 2, Fuel_Variety => Pumps.Fuel_95, State => Pumps.base, Price => 1.90, Reservoir => 100000, Active => False), 
     (ID => 3, Fuel_Variety => Pumps.Fuel_Diesel, State => Pumps.base, Price => 1.10, Reservoir => 60000, Active => False)); 

    Active_Pump:= 0; 

end Pump_Unit; 

Answer 1

Можно вызвать только функцию после того, как она была определена в целом (есть несколько исключений из этого правила, особенно для итераторов). В вашем случае, возможно, вы захотите добавить еще несколько публичных функций (которые не отображают тип вашего насоса). Например, как насчет:

function No_Active_Pump return Boolean 
    with Inline; 
function Is_Active (x : ID_Value) return Boolean 
    with Inline; 

procedure Lift_Nozzle(x: Shared_Types.ID_Value) 
    with Pre => No_Active_Pump and then 
      Get_Pump(x).State = base, 
     Post => Is_Active (x); 

private 
    function No_Active_Pump return Boolean 
     is (Get_Active_Pump = 0); 
    function Is_Active (x : ID_Value) return Boolean 
     is (Get_Pump (x).State = ready 
      and then Get_Active_Pump = x); 

Идея заключается в том, чтобы раскрыть некоторые функции, которые также могут быть полезны для пользователей пакета, если они должны писать свои собственные до и после, а не подвергая частные типы.