formal-methods - VDM 中的递归函数

Question

我将如何定义一个递归函数来找到比 VDM 中的输入数小二的最大幂？

功能如下：

最大：N -> N

到目前为止，我所拥有的是：

最大（n）=

if n=1 then 0
else if n=2 then 1
else ...最大（...）

Answer 1

这将类似于“其他一加这个数字的最大一半”。但由于这看起来有点像练习，我会让你弄清楚细节。