For a project I am currently trying to write a mini pilot assistance system for an imaginary aircraft. The task is to learn Ada Spark, not avionics. I have modelled the plane components I wish to use, done some tests in the main file to check the components work as expected, and all is fine, and now I am to add pre and post conditions to functions to make sure my plane is super safe. One such safety measure is to make sure the engine cannot be switched on whilst the plane is in tow, or vice versa, switch to tow whilst the engine is on.
I have modelled an engine as a highly complex record, with one attribute, type OnOff, which takes one of the values On, or Off. Note I plan on expanding upon the attributes, so it isn't going to remain a one attribute record.
Here is the engines specification file
package engines with SPARK_Mode
is
type OnOff is (On, Off);
type Engine is record
isOn: OnOff;
end record;
procedure switchOn (x : in out Engine);
procedure switchOff (x : in out Engine);
end engines;
My plane is put together like so:
type Plane is record
engine1: Engine;
engine2: Engine;
gearOfLanding: LandingGear;
doorPax1, doorPax2, doorServ1, doorServ2,
doorCockpit: Door;
panelOfReadings: ReadingsPanel;
panelOfAlerts: AlertsPanel;
planOfFlight: FlightPlan;
speedLimits: SpeedLimit;
altitudeLimits: AltitudeLimit;
attitudeLimits: AttitudeLimit;
litresPerMile: Integer;
fuelTank1: FuelTank;
end record;
The procedure switchOnEngine within the planes file takes an engine as an input and calls switchOn from the engines file. Here is the specification and below, the body:
procedure switchOnEngine (x : in out Engine; y : in Plane) with
Pre => y.panelOfReadings.mode /= Tow,
Post => x = (isOn => On) and y.panelOfReadings.mode /= Tow;
procedure switchOnEngine (x : in out Engine; y : in Plane)
is
begin
switchOn(x);
end switchOnEngine;
The plane is passed in as a variable so I can check various attributes for my pre and post conditions, but I am getting warning messages I am unsure how to resolve.
precondition might fail
cannot prove y.panelOfReadings.mode /= Tow e.g when .......mode =>Tow
The following line is also giving an error from the main file where I control my plane
switchOnEngine(AirForceOne.engine1, AirForceOne);
formal parameters x and y are aliased, and this is being marked as a 'high' priority warning.
here is the initialisation of the plane in the main file
AirForceOne : Plane := (
engine1 => (isOn => Off),
engine2 => (isOn => Off),
litresPerMile => 5,
gearOfLanding => (isExtended => Extended),
doorPax1 => (isClosed => Closed, isLocked => Unlocked),
doorPax2 => (isClosed => Closed, isLocked => Unlocked),
doorServ1 => (isClosed => Closed, isLocked => Unlocked),
doorServ2 => (isClosed => Closed, isLocked => Unlocked),
doorCockpit => (isClosed => Closed, isLocked => Unlocked),
fuelTank1 => (capacity=>26000, currentFuel=>26000),
planOfFlight => (distFromDest => 1500),
panelOfReadings =>
(mode => Tow,
currentSpeed => 0,
altitud => 0,
attitud =>
(currentPitch=>0,
currentRoll =>0)
),
panelOfAlerts =>
(approachingStallSpeed => Off,
unRestrictedSpeed => Off,
withinLandingSpdRange => Off,
withinOptCruiseAlt => Off,
withinOptCruiseSpeed => Off,
takeoffSpeedReached => Off,
fuelStatus => Off,
maxPitchAngleExceeded => Off,
maxRollAngleExceeded => Off),
speedLimits =>
(minLanding => 180,
maxLanding => 200,
minStall => 110,
minTakeoff => 130,
maxRestricted => 300,
maxGroundMode => 10),
altitudeLimits =>
(minFlight => 500,
maxFlight => 41000,
optCruiseAlt => 36000,
maxRestrictedSpeed => 10000,
maxInitiateFlareMode => 100),
attitudeLimits =>
(maxRoll => 30,
maxPitch => 30,
minRoll => -30,
minPitch => -30)
);
Any help would be great. I thought it would be enough to suggest in the pre condition that the plane cannot be in tow, but it seems to not be enough.
The purpose of Switchonengine is to change the state of the plane. Writing it to change the state of an engine is going to complicate things.
Max_Engines : constant := 100; -- The Lillium jet has 36, so I hope this is enough
type Engine_Num is range 1 .. Max_Engines;
type Engine_Info is ...
type Engine_Map is array (Engine_Num range <>) of Engine_Info with
Dynamic_Predicate => Engine_Map'First = 1;
type Plane_Info (Num_Engines : Engine_Num) is record
Engine : Engine_Map (1 .. Num_Engines);
...
procedure Turn_On (Engine : in Engine_Num; Plane : in out Plane_Info) with
Pre => Engine in 1 .. Plane.Num_Engines and then
(not Running (Plane.Engine (Engine) ) and not Under_Tow (Plane),
Post => Running (Plane.Engine (Engine) );
Air_Force_One : Plane_Info (Num_Engines => 4);