Prove globals about gneiss

[jklmnn]

The global state consists of the application state and the platform state. The platform state should have been modeled initially by the session objects. However this is not always possible as some modifications on the platform do not depend on changes in the session object. To model this an abstract Platform_State should be used which is then refined platform dependently.

The application state is fully visible to the application. However some procedures that access the application state but are called from within platform code. As this code is platform specific it cannot model global state correctly. There are two different scenarios:

• Procedures that are called by interrupts
  These procedures are entry points which means that they can be handled like public package procedures that might modify internal state but cannot have pre and post conditions that depend directly on internal state. Maybe we should only declare these procedure in the public part of package specifications. I don't know if we can enforce this somehow.
• Procedures that are called by API calls
  Some procedures are called when another procedure of the session is called. This means that application code and platform code may be intertwined. This means that global state needs to be modeled directly as calls can modify it within a procedure. As global state of generic formal parameters cannot be modeled in generic packages it can only be null. To still access application state procedures that call generic parameters are generic and get a limited private type. They also have an additional parameter of this type that is passed in out into the callee.

[jklmnn]

When trying to prove the globals I noticed that global state from a withed package must always be annotated to the procedure accessing it directly. As it is not hidden it cannot be refined. This leads to the problem that specs would have to import platform dependent units just to define their global state. I see two solutions:

• Define well known names for platform packages that include state. This can be cumbersome and it is always a trade-off between more flexibility against less implementation effort. It probably could be done by creating a platform wide top level package that defines an imported state and all other packages are children and their state is part of the parent state.
• Make all platform units generic. When a generic unit is instantiated in the body it is only visible there and therefor its state is hidden and can be refined. On the other hand this might lead to code duplication and more memory usage since data defined on package level will be instantiated, too. This might be a problem on embedded platforms.

[jklmnn]

For the first option I came up with the following idea:

package Platform with
   SPARK_Mode,
   Abstract_State => Platform_State
is
end Platform;

package body Platform with
   SPARK_Mode,
   Refined_State => (Platform_State => null)
is
end Platform;

private package Platform.Implementation with
   SPARK_Mode,
   Abstract_State => (Implementation_State with Part_Of => Platform.Platform_State)
is

   procedure Do_Something with
      Global => (In_Out => Implementation_State);

end Platform.Implementation;

package Platform.Definition with
   SPARK_Mode
is

   procedure Run with
      Global => (In_Out => Platform.Platform_State);

end Platform.Definition;

package body Platform.Definition with
   SPARK_Mode
is

   procedure Run
   is
   begin
      Platform.Implementation.Run;
   end Run;

end Platform.Implementation;

In this case if another unit wants to use a functionality of platform, its state will always be Platform.Platform_State. Since Platform.Implementation is a private package only child units of platform can with it inside their bodies. This makes the state of Platform.Implementation a hidden state and it is part of the refinement of Platform.Platform_State. Other units would only be allowed to use Platform.Definition. With this separation there might be an additional layer of abstraction but the state can be imported as a single entity while the actual implementation can be both public but also separated into multiple units.
@senier what are your thoughts about this?

[jklmnn]

Fixed by #173.