#integer #preconditions #formal-methods #vdm
#целое число #предварительные условия #формальные методы #vdm
Вопрос:
Допустим, у меня есть функция, которая возвращает меньшее из двух входных значений типа 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
?
Ответ №1:
Вы объявили функцию для приема аргументов типа 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
Чтобы получить поведение, которое вы видите, я должен отключить всю проверку динамического типа в параметрах проекта. Возможно, вы это сделали?
Комментарии:
1. Спасибо, что намекнули, что я, возможно, отключил всю проверку динамического типа. Потому что это именно то, что я сделал (ха-ха). Я использую VDM Toolbox Lite версии 8.0
2. VDMTools отлично подходит, хотя вы можете обнаружить, что Overture имеет более современный интерфейс и более знаком, если вы привыкли к Eclipse. github.com/overturetool/overture/releases/tag/Release/3.0.2