Re: a slight problem need some help. Simulation Control System

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 13 Nov, 16:09, "Mr.Spark" <malma...@gmail.com> wrote:
> I had a problem when I run examiner to check if the body package is
> working fine but the problem it gives me:
>
> Specification Part:
>
> with Sensor, Pump;
>
> --# inherit Sensor, Pump;
>
> package Tank
>
> --# own Tank_Level;
> --# initializes Tank_Level;
>
> is
>    procedure Control;
>
>    --# global out Tank_Level;
>    --#        in Sensor.Level;
>    --#        in out Pump.Pump_Open;
>    --# derives Tank_Level from Sensor.Level &
>    --#         Pump.Pump_Open from Sensor.Level, Pump.Pump_Open;
>
> end Tank;
>
> Body Package Is :
>
> with Sensor, Pump;
>
> package body Tank
>
> is
>
>    Empty: constant Sensor.Level_Type := 10;
>    Full: constant Sensor.Level_Type := 60;
>
>    -- this procedure controls the operation of pumps when they should
> be opened
>    -- or closed for the safety of the system. The pump will be closed
> if the
>    -- Water Level Tank is <= 10 and it will be Opened if the Water
> Level
>    -- in Tank >= 60.
>
>    procedure Control
>    is
>       Tank_Level: Sensor.Level_Type;
>    begin
>
>       Tank_Level:= Sensor.Get_Level;
>       if Tank_Level <= Empty then
>          Pump.Close;
>       elsif Tank_Level >= Full then
>          Pump.Open;
>       end if;
>    end Control;
>
> end Tank;
>
> The errors that it shows are :
>
> 1.Semantic Error : Ilegal redeclaration of identifier Tank_Level;
> 2.Semantic Error : The Identifier is either undeclared or not visible
> at his point
> 3.Semantic Error : The Identifier is either undeclared or not visible
> at his point1.
> 4.Semantic Error : The Identifier is either undeclared or not visible
> at his point
> 5.Semantic Error : The own variable Tank_Level does not have a
> definition
>
> If you could give me a hint how to solve this problem it would be
> great.

The main problem is that the 'own' annotation on the spec states that
the variable Tank_Level will be declared in the package body - as
permanent data.  But the code only creates it as local data within the
Control procedure.  So Tank_Level is created as uninitialised data
each time that the Control procedure is invoked.

If you move the declaration of Tank_Level to the package body then you
will remove some of the errors.  Alterntively if the data should be
local to the Control procedure then it should not be declared as 'own'
data in the package specification.

For more accurate error diagnosis, include at least the specs of all
the other referenced packages (ie Sensor and Pump in this case) so
that we can do a complete SPARK run.

Cheers,

Phil