从隐式到显式函数定义

Question

我一直在使用VDM中的隐式函数定义创建规范，并且效果非常好。现在，我希望使用显式函数定义(现阶段不进行操作)对规范进行原型化。

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

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

是否有从隐式函数定义转换为显式函数定义的推荐方法。长期而言，我确实想要正式地研究这一点，但首先，我只想实现隐式函数规范，以演示该规范的作用。

Answer 1

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

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

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