Ada使用私有函數的前提條件？

我對Ada非常陌生，對於在Ada規範文件中隱私保護我感到非常困惑。我有幾個私有函數需要保持私有，但我想在一些非私有過程中將它們用作前/後條件的一部分。當我嘗試給我們他們說它的功能是不確定的？Ada使用私有函數的前提條件？

我認爲使一個私人函數意味着它只能在該包內調用？即.ads和.adb文件？

以下是我的代碼到目前爲止。因此，我的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;

來源

2016-08-18 Josh2g

只能調用一個函數它一般被定義後（這個規則有一些例外，特別是迭代器）。就你而言，似乎你可能想添加一些公共功能（不公開你的泵類型）。舉例來說，有關如何：

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

這樣做是爲了揭露一些功能，如果他們需要編寫自己的前，後，雖然沒有暴露私有類型也可能是你的包的用戶非常有用。

來源

2016-08-18 08:18:31 manuBriot

Ada使用私有函數的前提條件？

回答

相關問題