SPARK 2016 Supports Ravenscar!
by Florian Schanda –
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 provedWhich means that all is proven and well! Enjoy the new feature! :)