Как да използвате предварително условие, за да гарантирате, че входовете са само от тип 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