VDM ++中有类型转换吗？

问题描述

例如，我要在VDM ++中将 nat 转换为 seq 。

在下面的代码中，如果q的类型为nat且q "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：

错误[207]：“ ^”的Rhs不是序列类型
行为：nat
exp：（＃seq1 | []）

解决方法

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

如果只想以纹理形式查看结果，则可以查看IO库，该库使您可以将各种类型的混合“打印”到控制台。另外，如果必须返回一个字符串，则可以指定一个将nat转换为十进制字符串的函数，然后返回“结果为” ^ nat2str（q）。