vdm++ - VDM++ 工具箱精简版上的未知错误

Question

我在 VDM++ toolbox lite 上做 VDM++，下面是我的示例代码：

class Course
types
public study :: numsubj : nat1
            sem : nat1;
public subjpersem = nat1;
operations
public getsubj:nat1 * nat1 ==>study
getsubj(numsubj,sem) == (
    subjpersem := numsubj/sem;
    );
end Course

我试图运行代码。成功创建对象，但是当我运行 print getsubj(10,2) 时，它返回错误 Run-Time Error 120: Unknown state component 有人可以帮我提前谢谢你

Answer 1

在 Overture/VDMJ 中，该规范给出了两个类型检查错误。这些没有出现在 VDMTools 中吗？

Error 3247: Symbol 'subjpersem' is not an updatable variable in 'Course' (test.vpp) at line 9:5
Error 3027: Operation returns unexpected type in 'Course' (test.vpp) at line 7:8
Actual: ()
Expected: study
Type checked 1 class in 0.119 secs. Found 2 type errors