Ada 编程/属性/'循环入口

描述

X'Loop_Entry [(loop_name)]

Loop_Entry 属性用于引用表达式在进入给定循环时的值，与子程序后置条件中的 Old 属性引用表达式在进入子程序时的值类似。相关循环要么由给定的循环名称标识，要么在没有给出循环名称时是内层封闭循环。

Loop_Entry 属性只能出现在 Assert、Assert_And_Cut、Assume、Loop_Variant 或 Loop_Invariant 编译指示中。此外，这样的编译指示必须是循环体语句序列中的项目之一，或者嵌套在循环体语句序列中出现的块语句中。Loop_Entry 的常见用途是在 Loop_Invariant 编译指示中比较对象的当前值与其在循环入口时的初始值。

使用 X'Loop_Entry 的效果与声明一个用 X 在循环入口时的初始值初始化的常量相同。如果循环没有进入，或者相应的编译指示被忽略或禁用，则不会执行此复制操作。