修正并填补VDM-SL中缺失的功能

Question

任务1： 下图显示了 IncubatorMonitor 系统的一组不完整的 VDM-SL 规范。该规范还包含语法、印刷和逻辑错误。

# values

# MAX_TEMP : int = 10;

# MIN_TEMP : int = -10;

# 

# state IncubatorMonitor

# temp: int

# inv mk_IncubatorMonitor(t) == t \>= MIN_TEMP and t \<= MAX_TEMP

# init IM == mk_IncubatorMonitor(5)

# end

# 

# operations

# Increment : () ==\> ()

# Increment () ==

# (temp := temp + 1)

# pre temp \< MAX_TEMP

# post temp = temp\~ + 1

使用 VDMTools 可以： • 纠正现有错误 • 填写缺失的功能

我尝试在 VDM-SL 中运行它，它给了我 2 个错误，但我无法添加新内容。

Answer 1

VDMTools 是一个相当古老的环境，不允许您直接编辑规范，除非您配置要使用的文本编辑器。

您可能会更幸运地使用 VDM-VSCode？