Ошибка типа 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в предварительном условии относится к возвращаемому значению.

Answer 2

Мне это кажется совершенно нормальным, и в VDM VSCode (1.2.1) или Overture (3.0.2) не сообщается об ошибках.

Какой инструмент вы используете?