VDM++工具箱lite上出现未知错误

Question

我正在VDM++工具箱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)时，它返回错误运行时错误120:未知状态组件是否有人可以帮助我提前感谢您

Answer 1

在Overture/VDMJ中，此规范给出了两个类型检查错误。

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