vdm-sl - 从隐式到显式的函数定义

Question

我一直在使用 VDM-SL 中的隐式函数定义创建规范，并且效果很好。我现在想使用显式函数定义对规范进行原型设计（此阶段没有操作）。

我可以看到的一种方法是创建一个新模块，该模块模仿隐式规范中定义的函数，但给它们显式定义。

我确信这可以做到，但我怀疑它是否理想。隐式规范和显式规范之间没有联系，尽管其中一个是对另一个的改进。

是否有从隐式转换到显式函数定义的推荐方法。从长远来看，我确实想正式研究这样做，但首先我只是想实现隐式函数规范以演示实际的规范。

Answer 1

细化规范有一个正式的过程，尽管它非常费力，特别是因为目前还没有工具支持它。

如果您保留隐式函数类型签名和前置/后置条件，那么显式版本“肯定”是一种改进，假设所有输入的实现都是正确的（这是组合测试可以提供帮助的地方）。请注意，您还可以为以“隐式”样式编写的函数提供实现（主体），这可以简化事情：

f(x:nat) r:nat
== x + 1        -- This line added to the implicit spec!
pre x > 10
post r < 100