SPARK 2016 supports Ravenscar!

by in Language, Formal Verification – November 12, 2015

We will try to demonstrate the new functionality through an example. For the sake of this example we will implement a simple traffic light and prove some of its functional behaviour. The functional behaviour that we will attempt to prove is that no pedestrians will be run over by vehicles (provided that drivers and pedestrians are aware of the traffic light's conventions and respect the signals). The system does not cater for suicidal behaviour or reckless driving. Other functional properties, like the sequence in which traffic lights alternate or the duration of each state of the traffic light, have not been proven. Given that this example was written in less than an hour I would advice against reusing the code in a real life traffic light system. :)
--  For the sake of this example the lights go as follows:
--
--  Vehicles                 Pedestrians
--
--  Green                    Red
--  Yellow                   Red
--  Red                      Green
--  Red and Yellow           Red
--
--  and over and over they go..

with Ada.Real_Time; use Ada.Real_Time;

package Traffic_Lights is
   protected Traffic_Light is
      function Valid_Combination return Boolean;

      entry Change_Lights
        with Post => Valid_Combination;

      procedure Check_Time;
   private
      --  The following holds the time when the last state change occurred.
      Last_State_Change : Time    := Time_First;

      --  The following is a boolean flag that indicates whether or not the
      --  time has arrived to change the state of the traffic light.
      Change_State      : Boolean := False;

      --  The following variables represent the actual lights of the traffic
      --  light. There are three lights for vehicles and two for pedestrians.
      --  When a variable is True the corresponding light is On. When a
      --  variable is False the corresponding light is Off.
      Vehicles_Green    : Boolean := False;
      Vehicles_Yellow   : Boolean := False;
      Vehicles_Red      : Boolean := True;
      Pedestrians_Green : Boolean := True;
      Pedestrians_Red   : Boolean := False;
   end Traffic_Light;

   task Check_The_Time;
   --  This task determines when it's time to change the traffic light.

   task Change_The_Lights;
   --  This task is periodically notified to change the traffic light.

end Traffic_Lights;
package body Traffic_Lights is
   protected body Traffic_Light is
      function Valid_Combination return Boolean is
        (if Vehicles_Green then
           not Vehicles_Yellow
           and not Vehicles_Red
           and not Pedestrians_Green
           and Pedestrians_Red

         elsif Pedestrians_Green then
           not Vehicles_Green
           and not Vehicles_Yellow
           and Vehicles_Red
           and not Pedestrians_Red

         else
           not Pedestrians_Green
           and Pedestrians_Red);


      entry Change_Lights when Change_State is
      begin
         pragma Assume (Valid_Combination);

         if Vehicles_Green then
            pragma Assert (not Vehicles_Red
                           and not Pedestrians_Green
                           and Pedestrians_Red);
            Vehicles_Green  := False;
            Vehicles_Yellow := True;

         elsif Vehicles_Yellow and not Vehicles_Red then
            pragma Assert (not Vehicles_Green);
            Vehicles_Yellow   := False;
            Vehicles_Red      := True;
            Pedestrians_Green := True;
            Pedestrians_Red   := False;

         elsif Vehicles_Red and not Vehicles_Yellow then
            pragma Assert (not Vehicles_Green
                           and Vehicles_Red);
            Vehicles_Yellow   := True;
            Pedestrians_Green := False;
            Pedestrians_Red   := True;

         elsif Vehicles_Red and Vehicles_Yellow then
            pragma Assert (not Pedestrians_Green
                           and Pedestrians_Red);
            Vehicles_Green  := True;
            Vehicles_Yellow := False;
            Vehicles_Red    := False;

         end if;

         Change_State := False;
         Last_State_Change := Clock;
      end Change_Lights;

      procedure Check_Time is
         Wait_Duration : constant Time_Span :=
           (if Vehicles_Yellow then
               --  States that involve a yellow vehicle light only last 2
               --  seconds.
               Seconds (2)
            else
               --  All other states last 15 seconds.
               Seconds (15));
      begin
         if Clock - Last_State_Change >= Wait_Duration then
            --  We have waited enough. It is time for a state change...
            Change_State := True;
         end if;
      end Check_Time;
   end Traffic_Light;

   task body Check_The_Time is
   begin
      loop
         Traffic_Light.Check_Time;
      end loop;
   end Check_The_Time;

   task body Change_The_Lights is
   begin
      loop
         Traffic_Light.Change_Lights;
      end loop;
   end Change_The_Lights;
end Traffic_Lights;
Writing the main subprogram is now easy, all we need to do is with the above package so that we trigger its elaboration. Our main will then wait for the tasks to terminate before it exits. That waiting will last until the end of time. Literally, because once Ada.Real_Time.Time reaches its maximum value pedestrians will have a problem, but by then we will no longer be around to assume the blame so all is good... :P
with Traffic_Lights; use Traffic_Lights;

procedure Let_There_Be_Traffic_Light is
begin
   --  Dummy main that just waits forever for the tasks of Traffic_Lights to
   --  terminate.
   null;
end Let_There_Be_Traffic_Light;
The output of the tools on the above example is:
traffic_lights.adb:25:13: info: assertion proved
traffic_lights.adb:32:13: info: assertion proved
traffic_lights.adb:39:13: info: assertion proved
traffic_lights.adb:46:13: info: assertion proved
traffic_lights.ads:19:22: info: postcondition proved
traffic_lights.ads:32:09: info: nontermination of task proved
traffic_lights.ads:36:09: info: nontermination of task proved
Which means that all is proven and well! Enjoy the new feature! :)
comments powered by Disqus