Блог

Допустим, у меня есть функция, которая возвращает меньшее из двух входных значений типа int . Я хочу установить предварительное условие так, чтобы разрешать только a и b типа int .

 class Example

functions
    min: int * int -> int
    min(a, b) ==
        if a < b
        then a
        else b
        -- The code below doesn't work
        -- pre varName1 = int

end Example
 

Когда я опускаю предварительное условие и ввожу print Example.min(12.345, 0.123) в интерпретатор, я получаю взамен 0.123.

Окно интерпретатора

Как мне гарантировать, что функция будет принимать только входные данные типа int ?

Вы объявили функцию для приема аргументов типа int . Попытка вызвать функцию с нецелочисленным аргументом является ошибкой проверки типа. Поэтому, когда я пытаюсь запустить это в Overture или VDMJ, вы получаете эту ошибку:

 Error 4075: Value 12.345 is not an integer in 'Example'
 

Вы, кажется, используете VDMTools? Я получаю следующее:

 >> print new Example().min(12.345, 0.123)
command line, l. 1, c. 13:
Run-Time Error 298: Incompatible types found in call of function/operation with dynamic type check
actual value: 12.345
expected type: int
 

Чтобы получить поведение, которое вы видите, я должен отключить всю проверку динамического типа в параметрах проекта. Возможно, вы это сделали?