Proof global state

[jklmnn]

Context and Problem

The session channels and functions are implemented as generic procedures in SPARK. They're called when the Run and Step procedures are called. However this also implies that the Run and Step procedures change that global state.

Let's assume a channel implementation:

with RFLX.RFLX_Builtin_Types;
with IO;

package Channel with
   SPARK_Mode
is

   procedure Send (Buffer : RFLX.RFLX_Builtin_Types.Bytes) with
      Global => (Output => IO.State);

   procedure Receive (Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
					  Length : out RFLX.RFLX_Builtin_Types.Length) with
      Global => (Input => IO.State);

   function Has_Data return Boolean with
      Global => (Input => IO.State);

end Channel;

generic
   ...
package RFLX.Test.Session
is

   procedure Run with
      Global => null;

end RFLX.Test.Session;

Using this in a RecordFlux session looks as follows:

with RFLX.Test.Session;
with Channel;

procedure Main with
   SPARK_Mode
is
   package Session is new RFLX.Test.Session (Channel.Send, Channel.Receive, Channel.Has_Data);
begin
   Session.Run;
end Main;

The problem here is that Session.Run modifies IO.State but this is not annotated.

Options

O1 Generate all states into the code

This would mean to generate all states that are used directly into the code:

with IO;

package RFLX.Test.Session
is

   procedure Run with
      Global => (In_Out => IO.State);

end RFLX.Test.Session;

+ No additional abstractions
+ Fine grained state descriptions

- Code has to be regenerated on every change in dependencies of the application
- Possibly a large number of states
- Requires an integration configuration for the code generation

O2 Create a global state for the Session and encapsulate all used states in private packages

This solution creates a separate package hierarchy that defines an abstract state that can be used to encapsulate other abstract states via private packages.

The root package will just define that state:

package RFLX_State with
   SPARK_Mode,
   Abstract_State => Session_State,
   Initializes => Session_State,
   Elaborate_Body
is
end RFLX_State;

package body RFLX_State with
   SPARK_Mode,
   Refined_State => (Session_State => null)
is
end RFLX_State;

The Session implementation will then just use this state:

with RFLX_State;

package RFLX.Test.Session
is

   procedure Run with
      Global => (In_Out => RFLX_State.Session_State);

end RFLX.Test.Session;

To use the channel it has to be encapsulated by a private package:

package RFLX_State.Channel with
   SPARK_Mode
is

   procedure Send (Buffer : RFLX.RFLX_Builtin_Types.Bytes) with
      Global => (Output => RFLX_State.Session_State);

   procedure Receive (Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
					  Length : out RFLX.RFLX_Builtin_Types.Length) with
      Global => (Input => RFLX_State.Session_State);

   function Has_Data return Boolean with
      Global => (Input => RFLX_State.Session_State);

end Channel;

with RFLX_State.IO_Channel;

package RFLX_State.Channel with
   SPARK_Mode
is

   procedure Send (Buffer : RFLX.RFLX_Builtin_Types.Bytes)
   is
   begin
      RFLX_State.IO_Channel.Send (Buffer);
   end Send;

   procedure Receive (Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
					  Length : out RFLX.RFLX_Builtin_Types.Length)
   is
   begin
      RFLX_State.IO_Channel.Receive (Buffer, Length);
   end Receive;

   function Has_Data return Boolean is (RFLX_State.IO_Channel.Has_Data);

end RFLX_State.Channel;

with RFLX.RFLX_Builtin_Types;
with IO;

private package RFLX_State.IO_Channel with
   SPARK_Mode,
   Abstract_State => (IO.State with Part_Of => RFLX_State.Session_State)
is

   procedure Send (Buffer : RFLX.RFLX_Builtin_Types.Bytes) with
      Global => (Output => IO.State);

   procedure Receive (Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
					  Length : out RFLX.RFLX_Builtin_Types.Length) with
      Global => (Input => IO.State);

   function Has_Data return Boolean with
      Global => (Input => IO.State);

end Channel;

The application has to use the channel implementation in RFLX_State then:

with RFLX.Test.Session;
with RFLX_State.Channel;

procedure Main with
   SPARK_Mode
is
   package Session is new RFLX.Test.Session
	  (RFLX_State.Channel.Send,
       RFLX_State.Channel.Receive,
       RFLX_State.Channel.Has_Data);
begin
   Session.Run;
end Main;

+ Simple implementation in the code generator
+ Flexible use of dependencies
+ No integration in the code generator required

- Additional abstraction layers
- More boiler plate code
- Coarse state descriptions