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 在迴圈入口時的初始值初始化的常量相同。如果迴圈沒有進入，或者相應的編譯指示被忽略或停用，則不會執行此複製操作。