VDM++类型错误:这里不能使用状态组件"totalPrice“

Question

我编写了一个代码，用于VDM++中的图书总价乘以图书数量和图书价格。

class Book

types
    public Title = seq of char;
    
instance variables
    private bookTitle: Title;
    private numberOfPages: nat1;
    private totalPrice : real;
    private price : real;
    private noofBook : nat1;
    
    inv numberOfPages >= 1 and numberOfPages <= 100;

values
    public Price: real = 20.50;

operations
    expCalculateTotalPrice: nat1 * real ==> real
    expCalculateTotalPrice (noofBook,price) ==
    ( 
        totalPrice := noofBook * price;
        return totalPrice;
    )

operations
    impCalculateTotalPrice(Book:real) price:real
      pre price > noofBook and price > 0
      post totalPrice = noofBook * price

end Book

错误是“状态组件"totalPrice”不能在这里使用“

post totalPrice = noofBook * price

这些有什么问题吗？

Answer 1

在隐式操作定义中需要外部访问声明，如下所示：

      ext
        rd noofBook:nat1
        wr totalPrice:real

如果您想要像显式版本那样写入实例变量totalPrice。

另一件可能使工具混淆的事情是名称崩溃。您的正式返回值price正在隐藏同名的实例变量，该工具可能会在前提条件下考虑返回值。