在VDM++中有类型铸造吗？

Question

例如，我希望将nat转换为char的seq in VDM++。

在下面的代码中，如果q是nat类型，并且q< 3，我希望操作setValueOfX返回"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

我尝试过使用^，但是我得到了下面的错误

Error207：“^”的Rhs不是序列类型 法案: nat 例：(#\\ []的seq1 )

Answer 1

不，您不能在VDM中隐式地转换这样的值。

如果您只想以纹理形式查看结果，可以查看IO库，它允许您将各种类型“打印”到控制台。或者，如果必须返回字符串，则可以指定将nat转换为十进制字符串的函数，返回“结果是”^ nat2str(q)。