X 在進入時的值，與 X 型別相同。
每個在啟用的後置條件表示式中的 X'Old，除了那些出現在被確定為未計算的子表示式中的 X'Old，都表示一個隱式地在子程式體、入口體或接受語句開始時宣告的常量。
X’Old return T
