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

Question

假设我有一个函数 return 类型为 int 的两个输入值中的较小者。我想将前提条件设置为只允许 int.

类型的 a 和 b

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)时，我在return中得到0.123。

Interpreter Window

如何确保函数只接受 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

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

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

How to use precondition to ensure that the inputs are of type int only

integer

formal-methods

preconditions

vdm++