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.

Go CodePeer!

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;