从隐式到显式的函数定义答案

【问题标题】：From implicit to explicit function definitions从隐式到显式的函数定义
【发布时间】：2016-02-08 20:27:03
【问题描述】：

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

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

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

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

【问题讨论】：

标签： vdm-sl

【解决方案1】：

有一个用于细化规范的正式流程，尽管它相当费力，尤其是因为目前还没有工具支持它。

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

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

【讨论】：