SPARK 2014 Rationale: Variables That Are Constant
by Florian Schanda –
Aspect Constant_After_Elaboration can be used on a library-level variable to indicate that the variable must retain the value that it has after elaboration of its enclosing package throughout the entire life of the program. This means that no user of the package is allowed to update the variable's value. The tools will issue warnings if the aspect is not respected. Since users of the package are prohibited from updating such variables, procedures that update them cannot be declared in the visible part of the package, they can only be declared in the package's body so that they can be used within the package itself. Let's have a quick look at some code:
package CAE is
Var : Integer := 0
with Constant_After_Elaboration;
procedure Illegal;
end CAE;
package body CAE is
procedure Illegal is
begin
Var := 10; -- Problem
end Illegal;
procedure Legal is
begin
Var := Var + 2; -- This is fine
end Legal;
begin
Var := Var + 1;
Legal;
end CAE;
with CAE; use CAE;
procedure User is
begin
Var := 5; -- Problem
end User;On the following code the tools issue two messages:
user.adb:3:11: high: constant after elaboration "Var" must not be an output of procedure "User"
cae.ads:5:14: high: constant after elaboration "Var" must not be an output of procedure "Illegal"These messages inform us that the Constant_After_Elaboration contract of Var has been violated. Notice that procedure Illegal cannot be called by a user of CAE without resulting in a violation of the Constant_After_Elaboration aspect. So having procedure Illegal appear in the visible part of CAE makes no sense. On the other hand, procedure Legal, which also does update Var, is perfectly OK since it is declared in the body of CAE and therefore can be used during the elaboration of package CAE but cannot be called from users of CAE. This is the reason why the tools issue a message on procedure Illegal but not on procedure Legal. This new feature is particularly useful when tasking code is involved. Variables which have aspect Constant_After_Elaboration set are guaranteed to be free of unsynchronised updates (since they are only ever updated during elaboration).