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;