检查变量的初始化
Check initialization of variable
在下面的代码示例中，变量 Time_Two 没有被初始化。这导致随机输出，如：
Time one: 2019-06-27 16:18:21
Time two: 2150-01-02 16:01:18
Ada 是否提供在运行时检查 Ada.Calendar.Time 类型的变量是否已初始化的函数？
with Ada.Calendar;
with Ada.Text_IO;
with GNAT.Calendar.Time_IO;
procedure Main is
Time_One : Ada.Calendar.Time := Ada.Calendar.Clock;
Time_Two : Ada.Calendar.Time;
Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";
begin
Ada.Text_IO.Put_Line ("Time one: " & GNAT.Calendar.Time_IO.Image
(Date => Time_One,
Picture => Format));
Ada.Text_IO.Put_Line ("Time two: " & GNAT.Calendar.Time_IO.Image
(Date => Time_Two,
Picture => Format));
end Main;
好吧，GNAT 确实发出警告：
warning: variable "Time_Two" is read but never assigned
通过将配置 pragma Warning_As_Error 放在 main.adb 的最顶部或配置文件 gnat.adc [GNAT RM 2.205 中，可以将警告转换为错误]
pragma Warning_As_Error ("*never assigned");
处理未初始化的变量是错误的常见来源，有关此主题的一些其他背景信息（特别关注使用 run-time 检查，如所要求）可在论文
Exposing Uninitialized Variables: Strengthening and Extending Run-Time Checks in Ada
有趣的是，将配置编译指示 Initialize_Scalars [GNAT RM 2.88] 放在 main.adb 的最顶部会产生（对于这种特殊情况）run-time 异常 Times_Two 用 Long_Long_Integer'First 初始化，这似乎对 Ada.Calendar.Time 无效（在 GNAT 中，Long_Long_Integer 是 Ada.Calendar.Time 的基础类型，参见 a-calend.ads）：
$ /main
Time one: 2019-06-27 19:46:54
raised ADA.CALENDAR.TIME_ERROR : a-calend.adb:611
当然，无效值可能不存在或可能具有不同的值。有关 Initialize_Scalars 用法的更多信息，请参阅 GNAT RM 的 link 和论文。另见相关编译指示 Normalize_Scalars [GNAT RM 2.122].
另一种检测未初始化变量的（静态）方法是使用 SPARK。尝试证明 main.adb 的正确性得到：
high: "Time_Two" is not initialized.
更新 1
这是一个最小的示例，说明如何将 pragma Initialize_Scalars 与 GNAT 编译器开关一起使用，在代码的特定点插入数据验证检查器：
main.adb
-- Ignore compile time warning for the sake of demonstration.
pragma Warnings (Off, "*never assigned");
pragma Initialize_Scalars;
with Ada.Text_IO;
procedure Main is
package Foo is
type Bar is private;
procedure Put_Bar (B : Bar);
private
type Bar is new Integer range -20 .. 20;
end Foo;
package body Foo is
procedure Put_Bar (B : Bar) is
begin
-- (2) Constraint_Error is raised if switch "-gnatVDo" (Validate
-- Operator and Attribute Operands) is used during compilation.
-- This switch effectively inserts the code
--
-- if not B'Valid then
-- raise Constraint_Error with "invalid data";
-- end if;
--
-- just before B'Image is evaluated. As the value Integer'First
-- is not in Bar'Range, B'Valid returns False and the
-- exception is raised.
--
-- See also in GPS IDE:
--
-- Edit > Project Properties... > Build > Switches > Ada
-- and then "Validity Checking Mode".
Ada.Text_IO.Put_Line (B'Image);
end Put_Bar;
end Foo;
-- (1) Because pragma "Initialize_Scalars" is used, B is deterministically
-- initialized to Integer'First. This behavior is inherited from the
-- configuration pragma "Normalize_Scalars" (see GNAT RM). Here,
-- Integer'First happens to be invalid as it falls outside the
-- range of subtype Foo.Bar (which is -20 .. 20).
B : Foo.Bar;
begin
Foo.Put_Bar (B);
end Main;
更新 2
第二个例子回应下面评论中的反馈（我误解了问题）：
main.adb
with Ada.Calendar;
with Ada.Text_IO;
with GNAT.Calendar.Time_IO;
procedure Main is
type Optional_Time (Valid : Boolean := False) is
record
case Valid is
when False =>
null;
when True =>
Value : Ada.Calendar.Time;
end case;
end record;
-----------
-- Image --
-----------
function Image (OT : Optional_Time) return String is
Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";
begin
if OT.Valid then
return GNAT.Calendar.Time_IO.Image (OT.Value, Format);
else
return "<Invalid>";
end if;
end Image;
Time : Optional_Time;
begin
Ada.Text_IO.Put_Line (Image (Time));
Time := (Valid => True, Value => Ada.Calendar.Clock);
Ada.Text_IO.Put_Line (Image (Time));
Time := (Valid => False);
Ada.Text_IO.Put_Line (Image (Time));
end Main;
按照第一个答案中的建议对包装器类型使用布尔判别式接近于回答问题，但从技术上讲，该技术只是区分具有值和不具有值，不一定能够检测是否变量未初始化。如果变量为non-default，则可以确定变量已初始化，但无法确定是否已初始化为默认值，或者在设置为non-default值后随后重置为默认值。
如果您想更准确地确定相应的日期值是否已 "initialized" ，另一种方法是定义一个无效值，并创建一个排除该值的子类型。可以创建一个抽象，默认将 holder/wrapper 类型初始化为具有无效值，但提供一个仅允许用户分配有效值的接口。那么在运行时间可以更准确的判断变量是否已经初始化。使持有者类型成为受限类型也进一步限制了使用，以防止将未初始化的值重新分配给已经初始化的变量。
例如
with Ada.Calendar;
with GNAT.Calendar.Time_IO;
package Initialized_Times is
use type Ada.Calendar.Time;
End_Of_Time : constant Ada.Calendar.Time
:= Ada.Calendar.Time_Of
(Year => Ada.Calendar.Year_Number'Last,
Month => Ada.Calendar.Month_Number'Last,
Day => Ada.Calendar.Day_Number'Last,
Seconds =>
Ada.Calendar.Day_Duration'Pred
(Ada.Calendar.Day_Duration'Last));
subtype Initialized_Time is Ada.Calendar.Time
with Dynamic_Predicate =>
Initialized_Time < End_Of_Time;
type Time_Holder is limited private;
Invalid_Time : constant Time_Holder;
function Create
(Value : Initialized_Time) return Time_Holder;
procedure Update (Date : in out Time_Holder;
Value : Initialized_Time);
function Image (OT : Time_Holder) return String;
function Time_Of
(Date : Time_Holder) return Initialized_Time;
function Is_Valid
(Date : Time_Holder) return Boolean;
private
type Time_Holder is limited
record
Value : Ada.Calendar.Time := End_Of_Time;
end record;
function Create
(Value : Initialized_Time) return Time_Holder is
(Value => Value);
function Time_Of
(Date : Time_Holder) return Initialized_Time is
(Date.Value);
function Image (OT : Time_Holder) return String is
((if Is_Valid (OT) then
GNAT.Calendar.Time_IO.Image
(OT.Value, "%Y-%m-%d %H:%M:%S")
else "<Invalid>"));
function Is_Valid
(Date : Time_Holder) return Boolean is
(Date.Value /= End_Of_Time);
Invalid_Time : constant Time_Holder :=
(Value => End_Of_Time);
end Initialized_Times;
---------------------------------------------
package body Initialized_Times is
procedure Update (Date : in out Time_Holder;
Value : Initialized_Time) is
begin
Date.Value := Value;
end Update;
end Initialized_Times;
-------------------------------------------------
with Ada.Calendar;
with Ada.Text_IO;
with Initialized_Times;
procedure Main is
Time : Initialized_Times.Time_Holder;
begin
Ada.Text_IO.Put_Line
(Initialized_Times.Image (Time));
Ada.Text_IO.Put_Line ("Time is " &
(if Initialized_Times.Is_Valid
(Date => Time) then ""
else "not ") &
"initialized.");
Initialized_Times.Update
(Date => Time,
Value => Ada.Calendar.Clock);
Ada.Text_IO.Put_Line ("Time is " &
(if Initialized_Times.Is_Valid
(Date => Time) then ""
else "not ") &
"initialized.");
Ada.Text_IO.Put_Line
(Initialized_Times.Image (Time));
end Main;
在下面的代码示例中，变量 Time_Two 没有被初始化。这导致随机输出，如：
Time one: 2019-06-27 16:18:21
Time two: 2150-01-02 16:01:18
Ada 是否提供在运行时检查 Ada.Calendar.Time 类型的变量是否已初始化的函数？
with Ada.Calendar;
with Ada.Text_IO;
with GNAT.Calendar.Time_IO;
procedure Main is
Time_One : Ada.Calendar.Time := Ada.Calendar.Clock;
Time_Two : Ada.Calendar.Time;
Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";
begin
Ada.Text_IO.Put_Line ("Time one: " & GNAT.Calendar.Time_IO.Image
(Date => Time_One,
Picture => Format));
Ada.Text_IO.Put_Line ("Time two: " & GNAT.Calendar.Time_IO.Image
(Date => Time_Two,
Picture => Format));
end Main;
好吧，GNAT 确实发出警告：
warning: variable "Time_Two" is read but never assigned
通过将配置 pragma Warning_As_Error 放在 main.adb 的最顶部或配置文件 gnat.adc [GNAT RM 2.205 中，可以将警告转换为错误]
pragma Warning_As_Error ("*never assigned");
处理未初始化的变量是错误的常见来源，有关此主题的一些其他背景信息（特别关注使用 run-time 检查，如所要求）可在论文
Exposing Uninitialized Variables: Strengthening and Extending Run-Time Checks in Ada
有趣的是，将配置编译指示 Initialize_Scalars [GNAT RM 2.88] 放在 main.adb 的最顶部会产生（对于这种特殊情况）run-time 异常 Times_Two 用 Long_Long_Integer'First 初始化，这似乎对 Ada.Calendar.Time 无效（在 GNAT 中，Long_Long_Integer 是 Ada.Calendar.Time 的基础类型，参见 a-calend.ads）：
$ /main
Time one: 2019-06-27 19:46:54
raised ADA.CALENDAR.TIME_ERROR : a-calend.adb:611
当然，无效值可能不存在或可能具有不同的值。有关 Initialize_Scalars 用法的更多信息，请参阅 GNAT RM 的 link 和论文。另见相关编译指示 Normalize_Scalars [GNAT RM 2.122].
另一种检测未初始化变量的（静态）方法是使用 SPARK。尝试证明 main.adb 的正确性得到：
high: "Time_Two" is not initialized.
更新 1
这是一个最小的示例，说明如何将 pragma Initialize_Scalars 与 GNAT 编译器开关一起使用，在代码的特定点插入数据验证检查器：
main.adb
-- Ignore compile time warning for the sake of demonstration.
pragma Warnings (Off, "*never assigned");
pragma Initialize_Scalars;
with Ada.Text_IO;
procedure Main is
package Foo is
type Bar is private;
procedure Put_Bar (B : Bar);
private
type Bar is new Integer range -20 .. 20;
end Foo;
package body Foo is
procedure Put_Bar (B : Bar) is
begin
-- (2) Constraint_Error is raised if switch "-gnatVDo" (Validate
-- Operator and Attribute Operands) is used during compilation.
-- This switch effectively inserts the code
--
-- if not B'Valid then
-- raise Constraint_Error with "invalid data";
-- end if;
--
-- just before B'Image is evaluated. As the value Integer'First
-- is not in Bar'Range, B'Valid returns False and the
-- exception is raised.
--
-- See also in GPS IDE:
--
-- Edit > Project Properties... > Build > Switches > Ada
-- and then "Validity Checking Mode".
Ada.Text_IO.Put_Line (B'Image);
end Put_Bar;
end Foo;
-- (1) Because pragma "Initialize_Scalars" is used, B is deterministically
-- initialized to Integer'First. This behavior is inherited from the
-- configuration pragma "Normalize_Scalars" (see GNAT RM). Here,
-- Integer'First happens to be invalid as it falls outside the
-- range of subtype Foo.Bar (which is -20 .. 20).
B : Foo.Bar;
begin
Foo.Put_Bar (B);
end Main;
更新 2
第二个例子回应下面评论中的反馈（我误解了问题）：
main.adb
with Ada.Calendar;
with Ada.Text_IO;
with GNAT.Calendar.Time_IO;
procedure Main is
type Optional_Time (Valid : Boolean := False) is
record
case Valid is
when False =>
null;
when True =>
Value : Ada.Calendar.Time;
end case;
end record;
-----------
-- Image --
-----------
function Image (OT : Optional_Time) return String is
Format : constant GNAT.Calendar.Time_IO.Picture_String := "%Y-%m-%d %H:%M:%S";
begin
if OT.Valid then
return GNAT.Calendar.Time_IO.Image (OT.Value, Format);
else
return "<Invalid>";
end if;
end Image;
Time : Optional_Time;
begin
Ada.Text_IO.Put_Line (Image (Time));
Time := (Valid => True, Value => Ada.Calendar.Clock);
Ada.Text_IO.Put_Line (Image (Time));
Time := (Valid => False);
Ada.Text_IO.Put_Line (Image (Time));
end Main;
按照第一个答案中的建议对包装器类型使用布尔判别式接近于回答问题，但从技术上讲，该技术只是区分具有值和不具有值，不一定能够检测是否变量未初始化。如果变量为non-default，则可以确定变量已初始化，但无法确定是否已初始化为默认值，或者在设置为non-default值后随后重置为默认值。
如果您想更准确地确定相应的日期值是否已 "initialized" ，另一种方法是定义一个无效值，并创建一个排除该值的子类型。可以创建一个抽象，默认将 holder/wrapper 类型初始化为具有无效值，但提供一个仅允许用户分配有效值的接口。那么在运行时间可以更准确的判断变量是否已经初始化。使持有者类型成为受限类型也进一步限制了使用，以防止将未初始化的值重新分配给已经初始化的变量。
例如
with Ada.Calendar;
with GNAT.Calendar.Time_IO;
package Initialized_Times is
use type Ada.Calendar.Time;
End_Of_Time : constant Ada.Calendar.Time
:= Ada.Calendar.Time_Of
(Year => Ada.Calendar.Year_Number'Last,
Month => Ada.Calendar.Month_Number'Last,
Day => Ada.Calendar.Day_Number'Last,
Seconds =>
Ada.Calendar.Day_Duration'Pred
(Ada.Calendar.Day_Duration'Last));
subtype Initialized_Time is Ada.Calendar.Time
with Dynamic_Predicate =>
Initialized_Time < End_Of_Time;
type Time_Holder is limited private;
Invalid_Time : constant Time_Holder;
function Create
(Value : Initialized_Time) return Time_Holder;
procedure Update (Date : in out Time_Holder;
Value : Initialized_Time);
function Image (OT : Time_Holder) return String;
function Time_Of
(Date : Time_Holder) return Initialized_Time;
function Is_Valid
(Date : Time_Holder) return Boolean;
private
type Time_Holder is limited
record
Value : Ada.Calendar.Time := End_Of_Time;
end record;
function Create
(Value : Initialized_Time) return Time_Holder is
(Value => Value);
function Time_Of
(Date : Time_Holder) return Initialized_Time is
(Date.Value);
function Image (OT : Time_Holder) return String is
((if Is_Valid (OT) then
GNAT.Calendar.Time_IO.Image
(OT.Value, "%Y-%m-%d %H:%M:%S")
else "<Invalid>"));
function Is_Valid
(Date : Time_Holder) return Boolean is
(Date.Value /= End_Of_Time);
Invalid_Time : constant Time_Holder :=
(Value => End_Of_Time);
end Initialized_Times;
---------------------------------------------
package body Initialized_Times is
procedure Update (Date : in out Time_Holder;
Value : Initialized_Time) is
begin
Date.Value := Value;
end Update;
end Initialized_Times;
-------------------------------------------------
with Ada.Calendar;
with Ada.Text_IO;
with Initialized_Times;
procedure Main is
Time : Initialized_Times.Time_Holder;
begin
Ada.Text_IO.Put_Line
(Initialized_Times.Image (Time));
Ada.Text_IO.Put_Line ("Time is " &
(if Initialized_Times.Is_Valid
(Date => Time) then ""
else "not ") &
"initialized.");
Initialized_Times.Update
(Date => Time,
Value => Ada.Calendar.Clock);
Ada.Text_IO.Put_Line ("Time is " &
(if Initialized_Times.Is_Valid
(Date => Time) then ""
else "not ") &
"initialized.");
Ada.Text_IO.Put_Line
(Initialized_Times.Image (Time));
end Main;