integer - 如何使用前置条件确保输入仅为 int 类型

Question

假设我有一个函数返回 type 的两个输入值中的较小者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 作为回报。

解释器窗口

如何确保该函数只接受 type 的输入int？

Answer 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

为了得到你看到的行为，我必须关闭项目选项中的所有动态类型检查。也许你已经这样做了？