Challenge 6 – Generated preconditions and postconditions
This electronic coaching program helps you monitor your (daily? weekly? not even?) running activities by automatically following a training program of your choice.
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 58: “postcondition of Start does not initialize T.Start”
Here’s how CodePeer helps you coming to this conclusion: As its name suggests, procedure Start is supposed to initiate the training, which supposes initializing Time fields of the training T. CodePeer generates the postcondition that T.Stop is initialized after calling Start, but it does not say anything about T.Start.
Error line 66: “Repeat only works under strange preconditions”
Here’s how CodePeer helps you coming to this conclusion: CodePeer generates the precondition that Num <= 14 for procedure Repeat. This means that you cannot choose to repeat an item an arbitrary number of times, which is quite odd given that the Count field of record type Item is of type Positive. This is because Repeat's implementation wrongly copies the item It given in argument instead of increasing its Count field.
Error line 74: “Skip does not work when there is only one item left”
Here’s how CodePeer helps you coming to this conclusion: CodePeer generates the precondition that T.Num_Items >= 2 for procedure Skip. This means that you should not call Skip with one item left, which corresponds to T.Num_Items = 1. Indeed, Skip removes the next item from the training, which must always contain at least one item (by typing constraint), so the procedure would raise an exception if called on a training with only one item left.
Error line 99: “warning: test always true because Change <= Current”
Here’s how CodePeer helps you coming to this conclusion: There was a typo in the definition of Change, which is defined as a subtraction instead of an addition. CodePeer detects that this causes Change to be always lower than Current, hence the warning.
package Coach is
type Time is new Natural; -- Time in seconds
type Speed is new Natural; -- Speed in meters per second
function "*" (Num : Positive; T : Time) return Time;
type Exercise is record
Length : Time; -- Duration of the exercise
Pace : Speed; -- Pace at which to run during this exercise
end record;
type Exercise_Ref is new Positive range 1 .. 200;
Catalogue : array (Exercise_Ref) of Exercise;
type Item is record
Ref : Exercise_Ref; -- Reference of an exercise in the catalogue
Count : Positive; -- Number of times to repeat the exercise
end record;
type Item_Ref is new Positive;
type Program is array (Item_Ref range <>) of Item;
subtype Program_Size is Item_Ref range 1 .. 15;
-- A training is a series of exercises that can be modulated along the way
type Training (Num_Items : Program_Size := 1) is record
Prog : Program (1 .. Num_Items); -- Program for the training
Start : Time; -- Starting time of the program
Stop : Time; -- Expected time of completion
end record;
-- Let's go! Start the program at the current time.
procedure Start (T : in out Training; Current : Time);
-- I'm feeling good. Change the program to repeat the item It a number
-- Num of times.
procedure Repeat (T : in out Training; It : Item_Ref; Num : Positive);
pragma Precondition (It <= T.Num_Items);
-- I am running late. Change the program to skip the current item.
procedure Skip (T : in out Training);
-- I am dead! Change the program to skip the next N items.
procedure Skip_N (T : in out Training; Num : Positive);
-- Where am I? Update the program based on time elapsed since last item.
procedure Update (T : in out Training; Elapsed : Time);
end Coach;
package body Coach is
function "*" (Num : Positive; T : Time) return Time is
begin
return Time (Num) * T;
end "*";
procedure Start (T : in out Training; Current : Time) is
begin
T.Stop := Current;
for J in T.Prog'Range loop
T.Stop := T.Stop + Catalogue (T.Prog (1).Ref).Length;
end loop;
end Start;
procedure Repeat (T : in out Training; It : Item_Ref; Num : Positive) is
begin
for J in 1 .. Num loop
T.Prog (It + Item_Ref (J)) := T.Prog (It);
end loop;
T.Stop := T.Stop + Num * Catalogue (T.Prog (It).Ref).Length;
end Repeat;
procedure Skip (T : in out Training) is
Skipped : constant Time :=
T.Prog (1).Count * Catalogue (T.Prog (1).Ref).Length;
begin
for J in 1 .. T.Prog'Last - 1 loop
T.Prog (J) := T.Prog (J + 1);
end loop;
T := Training'(Num_Items => T.Num_Items - 1,
Prog => T.Prog (1 .. T.Num_Items - 1),
Start => T.Start,
Stop => T.Stop - Skipped);
end Skip;
procedure Skip_N (T : in out Training; Num : Positive) is
begin
for J in 1 .. Num loop
Skip (T);
end loop;
end Skip_N;
procedure Update (T : in out Training; Elapsed : Time) is
Change : constant Time :=
T.Start - T.Prog (1).Count * Catalogue (T.Prog (1).Ref).Length;
Current : constant Time := T.Start + Elapsed;
begin
if Current >= Change then
Skip (T); -- Switch to the next exercise
T.Start := Current; -- Record the starting time for the new exercise
end if;
end Update;
end Coach;