Challenge 9 – Checking User-Specified Contracts
Ever wondered how a drowsy pilot might react to wings having bad vibrations on a diverging plane? Well, let’s explore the possibilities in this small automaton with 3^5 states.
Have a look at the following code and see if you can spot the errors. Once you think you’ve got them all, click on the “Go CodePeer” button to see how well you matched up to CodePeer’s comprehensive and rapid analysis of the same code.
Error line 74: “high: postcondition failure on wings.decrease_stress: requires Current_State <= Under_Stress”
Here’s how CodePeer helps you coming to this conclusion: Decrease_Stress is annotated with a contract expressed as a pair of aspects “Pre” and “Post” in Ada 2012 syntax. CodePeer detects that the postcondition of this contract is violated. Indeed, Decrease_Stress starts in a state where Current_State is not minimal, then it is incremented, so it cannot end with Normal_Condition or Under_Stress, which is required by its postcondition. The problem is that the increment on line 73 should really be a decrement.
Error line 111: “medium: precondition might fail on plane.transition: requires (soft) New_State = In_Distress”
Here’s how CodePeer helps you coming to this conclusion: Procedure Plane. Transition has a precondition expressed in Ada 2012 syntax, with a “Pre” aspect. It says that argument New_State should be equal to In_Distress whenever the Current_State is so. Here, it might be the case, so the caller should not be allowed to call Plane.Transition with New_State = On_Trajectory.
Error line 122: “high: precondition failure on wings.transition: requires New_State = Under_Stress or Current_State = Under_Stress”
Here’s how CodePeer helps you coming to this conclusion: CodePeer computes the precondition that either one of parameter New_State or global Current_State must be equal to Under_Stress when calling Wings.Transition. This precondition directly originates in a user assertion in Wings.Transition. On line 122, neither is true: Current_State is equal to Bad_Vibration according to the test on line 121, and the parameter New_State is equal to Normal_Condition.
Error line 144: “warning: dead code because New_State >= Drowsy”
Here’s how CodePeer helps you coming to this conclusion: CodePeer detects that New_State cannot be equal to Awake at this point. Assume that Transition is called with New_State = Awake. It returns on line 133 if Current_State = Awake. Otherwise, Current_State /= Awake and Transition calls Treat_Emergency on line 138, which requires in precondition that Current_State = Awake (through a pragma Precondition). This is impossible, which CodePeer correctly detects and transforms into a precondition on Transition, requiring that Current_State <= New_State.
Error line 146: “medium: precondition might fail on plane.transition: requires (soft) New_State = In_Distress”
Here’s how CodePeer helps you coming to this conclusion:This is the same error as on line 111.
package Engines is
type State is (Excessive_Speed, Normal_Speed, Halted);
Current_State : State;
procedure Transition (New_State : State);
end Engines;
package Plane is
type State is (On_Trajectory, Diverging, In_Distress);
Current_State : State;
procedure Transition (New_State : State) with
Pre => (if Current_State = In_Distress then New_State = In_Distress);
-- State 'In_Distress' is sticky, no action should change it
end Plane;
package body Plane is
procedure Transition (New_State : State) is
begin
Current_State := New_State;
end Transition;
end Plane;
package Tank is
type State is (Full, Half_Full, Empty);
Current_State : State;
procedure Transition (New_State : State);
end Tank;
package Wings is
type State is (Normal_Condition, Under_Stress, Bad_Vibration);
Current_State : State;
function Stress_Is_Minimal return Boolean is
(Current_State = Normal_Condition);
function Stress_Is_Maximal return Boolean is
(Current_State = Bad_Vibration);
procedure Increase_Stress with
Pre => not Stress_Is_Maximal,
Post => not Stress_Is_Minimal;
procedure Decrease_Stress with
Pre => not Stress_Is_Minimal,
Post => not Stress_Is_Maximal;
procedure Transition (New_State : State);
end Wings;
package body Wings is
procedure Increase_Stress is
begin
Current_State := State'Val (State'Pos (Current_State) + 1);
end Increase_Stress;
procedure Decrease_Stress is
begin
Current_State := State'Val (State'Pos (Current_State) + 1);
end Decrease_Stress;
procedure Transition (New_State : State) is
begin
pragma Assert
(New_State = Under_Stress or else Current_State = Under_Stress);
-- No abrupt transition should be observed from 'Normal_Condition' to
-- 'Bad_Vibration' directly, or the opposite way
Current_State := New_State;
end Transition;
end Wings;
package Pilot is
type State is (Awake, Drowsy, Asleep);
Current_State : State;
procedure Transition (New_State : State);
end Pilot;
with Engines; use type Engines.State;
with Plane; use type Plane.State;
with Tank; use type Tank.State;
with Wings; use type Wings.State;
package body Pilot is
procedure Recover_Trajectory is
begin
if Engines.Current_State = Engines.Normal_Speed and then
Tank.Current_State /= Tank.Empty and then
Wings.Current_State = Wings.Normal_Condition then
-- Eventually recover the planned trajectory, if not currently
Plane.Transition (Plane.On_Trajectory);
end if;
end Recover_Trajectory;
procedure Treat_Emergency is
pragma Precondition (Current_State = Awake);
begin
if Engines.Current_State /= Engines.Normal_Speed and then
Tank.Current_State /= Tank.Empty then
-- Get back to normal state when possible
if Wings.Current_State = Wings.Bad_Vibration then
Wings.Transition (Wings.Normal_Condition);
end if;
if Engines.Current_State = Engines.Excessive_Speed then
Engines.Transition (Engines.Normal_Speed);
end if;
end if;
end Treat_Emergency;
procedure Transition (New_State : State) is
begin
if New_State = Current_State then
return;
end if;
-- If not asleep, then the pilot can recover from an emergency
if New_State /= Asleep then
Treat_Emergency;
end if;
-- It requires the pilot to be fully awake to recover the trajectory,
-- otherwise the plane just drifts away
if New_State = Awake then
Recover_Trajectory;
else
Plane.Transition (Plane.Diverging);
end if;
Current_State := New_State;
end Transition;
end Pilot;