casting - VDM++ 中有类型转换吗？

Question

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

"X is {value of q}"在下面的代码中，如果 q 是 nat 类型并且 q < 3 ，我希望操作 setValueOfX 返回。

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

我试过使用^，但出现以下错误：

错误 [207] : '^' 的 Rhs 不是序列类型
行为: nat
exp : ( seq1 of # | [] )

Answer 1

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

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