X 在进入时的值，与 X 类型相同。
每个在启用的后置条件表达式中的 X'Old，除了那些出现在被确定为未计算的子表达式中的 X'Old，都表示一个隐式地在子程序体、入口体或接受语句开始时声明的常量。
X’Old return T
