VDM++出现The state component "totalPrice" must not be used here报错是什么原因？

错误触发行：post totalPrice = noofBook * price
错误提示：The state component "totalPrice" must not be used here

• 第一个原因是缺少状态修改权限声明：VDM++要求所有操作必须通过ext子句显式声明需要读写的类实例变量，你要在impCalculateTotalPrice操作中修改totalPrice变量，必须在pre子句前添加ext write totalPrice : real声明写入权限，未声明的情况下直接在post子句中引用状态变量会触发校验错误。
• 第二个原因是后置状态变量的语法使用错误：在隐式操作的post子句中，引用操作执行之后的实例变量值，必须在变量名后添加~后缀，未加后缀的变量名默认指代操作执行前的旧状态值。你当前的逻辑是要约定操作执行后totalPrice等于书籍数量乘以单价，正确的写法应为post totalPrice~ = noofBook * price，直接写totalPrice不符合语法规则。

附加代码问题提示 #

• 你当前的impCalculateTotalPrice操作签名定义不规范，不符合VDM++隐式操作的签名格式，如果你要定义接收书籍数量、单价两个入参并返回总价的隐式操作，正确的签名格式应和前面的显式操作保持一致：impCalculateTotalPrice: nat1 * real ==> real
• 你当前pre子句中的price > noofBook约束没有业务合理性，属于冗余的错误校验逻辑，可以根据实际业务需求调整。

内容的提问来源于stack exchange，提问作者Ninja Muffin