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
Hi Phil,
Thanks a lot for replying in a short time. I Appreciate your help.
that solved the problem. :)