使用VDM++ Toolbox Lite遇运行时错误120，请求技术帮助

我来帮你分析下报错的根源，然后给出针对性的修复方案：

错误原因拆解 #

你的代码里有两个核心问题触发了这个运行时错误：

1. subjpersem是类型别名而非状态变量：你在types块里定义的public subjpersem = nat1;只是把subjpersem声明成了nat1的类型别名，并不是类的状态组件（也就是实例变量）。VDM++里只有在state块中定义的元素才是对象的可赋值状态属性，直接给类型别名赋值自然会报“未知状态组件”的错误。
2. getsubj操作缺少返回值：你的操作声明是getsubj:nat1 * nat1 ==>study，明确要求返回一个study类型的值，但当前代码里没有任何返回语句，这也会导致运行时异常。

修正后的完整代码 #

下面是修复后的代码，我标注了关键修改点：

class Course
types
public study :: numsubj : nat1 sem : nat1;
public subjpersem = nat1;  // 保留类型别名，用于标记单学期课程数的类型
state  // 新增state块，定义对象的状态组件
public
  currentSubjPerSem : subjpersem;  // 用subjpersem类型定义可赋值的状态变量
operations
public getsubj:nat1 * nat1 ==>study
getsubj(numsubj,sem) == (
  currentSubjPerSem := numsubj div sem;  // 用div做整数除法（VDM++中/是浮点数除法，nat1需要整数结果）
  return mk_study(numsubj, sem);  // 返回study类型的构造值，匹配操作的返回类型声明
);
end Course

关键修改说明 #

• 新增state块：定义了currentSubjPerSem作为合法的状态变量，让操作里的赋值有了正确的目标。
• 替换除法运算符：把/改成div，因为numsubj和sem都是正整数类型，div会返回整数结果，避免类型不匹配的问题。
• 添加返回语句：用mk_study构造study类型的实例并返回，严格匹配操作声明的返回类型要求。

测试验证 #

重新编译代码并创建Course对象后，执行print getsubj(10,2)，应该会返回mk_study(10,2)，同时对象的currentSubjPerSem状态会被设置为5，不会再出现运行时错误。

内容的提问来源于stack exchange，提问作者Fadhil Adzfar