Is there type casting in VDM++?

Question

For example, I want to cast nat to seq of char in VDM++.

In the code below, I want operation setValueOfX to return "X is {value of q}", if q is of type nat and q < 3.

class A1

instance variables
    private x : nat := 0;


operations
    
    public setValueOfX : nat ==> seq of char
        setValueOfX(q) ==
        (
            if is_nat(q) and q < 3
                then
                (
                    x := q;

                    -- The following line doesn't work
                    -- return "X is " ^ q;
                )
            else
                return "Invalid value! Value of x must be more than 0 and less than 3.";
        );

end A1

I've tried using ^ but I got the following error:

Error[207] : Rhs of '^' is not a sequence type
act : nat
exp : ( seq1 of # | [] )

Answer 1

No, you can't implicitly convert values like that in VDM.

If you just want to see the result in a textural form, you could look at the IO library, which lets you "print" a mixture of types to the console. Alternatively, if you must return a string, you could specify a function that converts a nat to a decimal string, and the return "Result is" ^ nat2str(q).