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

Question

Let say I have a function that return the lesser of two input values of type int. I want to set the precondition to only allow a and b of type 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

When I omit the precondition and enter print Example.min(12.345, 0.123) in the interpreter, I got 0.123 in return.

Interpreter Window

How do I ensure that the function will only accept inputs of type int?

Answer 1

You have declared the function to take arguments of type int. It is a type-checking error to attempt to call the function with a non-integer argument. So when I attempt to launch this in Overture or VDMJ, you get that error:

Error 4075: Value 12.345 is not an integer in 'Example'

You seem to be using VDMTools? I get the following:

>> 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

To get the behaviour you see, I have to turn OFF all the dynamic type checking in Project Options. Perhaps you have done this?