ada - 在下面的 ADA Spark 示例中,我如何阻止先决条件失败
问题描述
对于一个项目,我目前正在尝试为想象中的飞机编写一个小型飞行员辅助系统。任务是学习 Ada Spark,而不是航空电子设备。我已经对我希望使用的飞机组件进行了建模,在主文件中进行了一些测试以检查组件是否按预期工作,一切都很好,现在我要在函数中添加前置条件和后置条件以确保我的飞机是超级的安全的。一种这样的安全措施是确保在飞机被拖曳时不能打开发动机,反之亦然,在发动机打开时切换到拖曳。
我将引擎建模为高度复杂的记录,具有一个属性,类型 OnOff,它采用值 On 或 Off 之一。注意我计划扩展属性,所以它不会保留一个属性记录。
这是引擎规范文件
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;
我的飞机是这样组装的:
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;
planes 文件中的过程 switchOnEngine 将引擎作为输入,并从引擎文件中调用 switchOn。这是规格,下面是正文:
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;
飞机作为变量传入,因此我可以检查我的前后条件的各种属性,但我收到警告消息,我不确定如何解决。
precondition might fail
cannot prove y.panelOfReadings.mode /= Tow e.g when .......mode =>Tow
以下行也从我控制我的飞机的主文件中给出错误
switchOnEngine(AirForceOne.engine1, AirForceOne);
formal parameters x and y are aliased, and this is being marked as a 'high' priority warning.
这是主文件中飞机的初始化
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)
);
任何帮助都会很棒。我认为在飞机不能被拖曳的前提下建议就足够了,但似乎还不够。
解决方案
的目的Switchonengine
是改变飞机的状态。编写它来改变引擎的状态会使事情复杂化。
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);
推荐阅读
- java - Java:打印出整数数组的最长序列。问题出在哪里?
- java - 如何在android studio(java)中使用单击方法从圆形图像视图中显示另一个活动/片段中的图像?
- vue.js - 如何显示我的 Stripe 默认错误?
- python - tensorflow2.0逻辑模型每次输出nan weight和bias
- python - 连接到 Azure AD 时如何创建客户端断言 JWT 令牌?
- c++ - 用 lambda 对对象向量进行排序,最后不排序
- sql - Azure SQL:是否可以使用来自另一个数据库的视图?
- javascript - 如何创建响应式网格布局,如 unsplash.com,内容不断变化 - React js
- java - 使用泛型 java 类型参数类
- laravel - 如何将新用户重定向到编辑个人资料页面