Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

a slight problem need some help. Simulation Control System

2 views
Skip to first unread message

Mr.Spark

unread,
Nov 13, 2009, 11:09:01 AM11/13/09
to
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.

Phil Thornley

unread,
Nov 13, 2009, 11:54:27 AM11/13/09
to

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

Mr.Spark

unread,
Nov 14, 2009, 4:06:46 AM11/14/09
to
On Nov 13, 4:54 pm, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:

Hi Phil,

Thanks a lot for replying in a short time. I Appreciate your help.
that solved the problem. :)


0 new messages