VDM++ 有类型转换吗？

Question

例如，我想在 VDM++ 中将 nat 转换为 char 的 seq。

在下面的代码中，如果 q 的类型为 nat 并且 q < 3.

，我希望操作 setValueOfX 为 return "X is {value of q}"

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

我试过使用 ^ 但我得到以下结果 error:

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

Answer 1

不，您不能像 VDM 中那样隐式转换值。

如果您只想以文本形式查看结果，可以查看 IO 库，它可以让您将多种类型“打印”到控制台。或者，如果您必须 return 一个字符串，您可以指定一个将 nat 转换为十进制字符串的函数，并且 return "Result is" ^ nat2str(q).