Как использовать предварительное условие, чтобы гарантировать, что входные данные имеют тип только int

Допустим, у меня есть функция, которая возвращает меньшее из двух входных значений типа 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?


integer formal-methods preconditions vdm++
person ariessa    schedule 23.11.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вы объявили функцию, которая принимает аргументы типа 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

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

person Nick Battle    schedule 24.11.2020
comment
Спасибо, что намекнули, что я мог отключить всю динамическую проверку типов. Потому что именно это я и сделал (ха-ха). Я использую VDM++ Toolbox Lite v8.0. - person ariessa; 24.11.2020
comment
С VDMTools все в порядке, хотя вы можете обнаружить, что Overture имеет более современный интерфейс и более знаком, если вы привыкли к Eclipse. github.com/overturetool/overture/releases/tag/Release%2F3. 0,2 - person Nick Battle; 24.11.2020