内隐和外显在VDM-SL中的区别是什么？

Question

因此，正如标题所解释的，内隐和外显之间有什么区别？函数是隐式的还是显式的？或者是隐含的序曲代码和显式的VDM规范本身？我有点困惑

Answer 1

隐式定义是指函数或操作仅通过(预和)后置条件(即布尔表达式)定义的地方。它没有说明如何达到后置条件中的结果(尽管它通过给出结果的显着性来暗示它)。此类功能和操作不能由解释器常规执行，但在指定合同(假设和保证)时完全有效。

显式函数或操作的主体给出了如何计算结果的命令式定义，因此可以由解释器执行。