CODEWITHSUNDEEP
privateencapsulationada
Josh2g
Josh2g

Reputation: 11

Ada preconditions that use private functions?

I am very new to Ada, I am really confused about making things private in an Ada spec file. I have a few private functions which need to stay private but I want to use them as part of pre/post conditions in some of my non-private procedures. When I try to us them it says the function is undefined ?

I thought that making a function private means it is only available to call within that package ?? i.e. both the .ads and .adb file?

Below is my code so far. So my pre/post conditions of my Lift_Nozzle procedure use the private functions Get_Active_Pump and Get_Pump, but when I check the semantic it says they are undefined (because they are private ?). Is there a work around for this ? Thanks

pump_unit.ads (some of it):

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 (some of it):

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;

Upvotes: 1

Views: 634

Answers (1)

manuBriot
manuBriot

Reputation: 2715

You can only call a function after it has been defined in general (there are a few exceptions to this rule, notably for iterators). In your case, it seems you might want to add a few more public functions (that do not expose your Pump type). For instance, how about:

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

The idea is to expose some functions that might also be useful for users of your package if they need to write their own pre and post, while not exposing private types.

Upvotes: 7

Related Questions