0

我写了一个代码，它是书籍总价格乘以书籍数量和 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

这些有什么问题？

4

2 回答 2

1

您需要在隐式操作定义中进行外部访问声明，例如：

      ext
        rd noofBook:nat1
        wr totalPrice:real

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

可能使该工具感到困惑的另一件事是名称崩溃。您的正式返回值price隐藏了同名的实例变量，并且该工具可能会认为price前置条件中的 指的是返回值。

于 2021-12-06T09:56:45.323 回答
0

这在我看来完全没问题，并且在 VDM VSCode (1.2.1) 或 Overture (3.0.2) 中没有报告错误。

你用的是什么工具？

于 2021-12-06T09:18:48.017 回答