VDMSL 递归函数序列的最小值答案

【问题标题】：VDMSL Recursive function minimum value of sequenceVDMSL 递归函数序列的最小值
【发布时间】：2014-06-02 21:55:00
【问题描述】：

我认为这应该相对简单，想知道是否有人知道如何回答这个问题：

定义一个递归函数 seq-min : N+ -> N 返回自然数序列中的最小值。

我在想一些类似的事情......

if hd seq < hd tl seq then seq-min([hd seq] concat tl tl seq)
else if hd seq > hd tl seq then seq-min(tl seq)
else if hd seq = hd tl seq then seq-min(tl seq)

感谢您的帮助！

【问题讨论】：

你可以看到这个问题：因为它正在测试值对，并在列表的尾部递归，最终它将传递一个单值序列。那时，“hd tl seq”将失败。下面的答案通过递归传递最小“向下”并仅测试头部来避免对对的需要。

标签： recursion sequence formal-methods vdm++ vdm-sl

【解决方案1】：

这是一个稍微不同的方法，使用一个函数：

    seq_min: seq of nat -> nat
    seq_min(s) ==
            cases s:
                    [x] -> x,

                    [x] ^ rest ->
                            let min = seq_min(rest) in
                                    if x < min then x else min
            end
    pre len s > 0;

它的优点是简短直观（并且功能单一）。当规范写成这样的案例表达式中的一组“模式”时，规范可以非常清晰，因为每个案例都明确地“解释”了。

【讨论】：

【解决方案2】：

类似的方法可能会奏效，但很难遵循 - 我们正在编写规范，所以如果它很清楚会有所帮助。以下是我的第一个想法。用了两个函数有点作弊，但希望比较清楚：

    seq_min: seq of nat -> nat
    seq_min(s) ==
            minrec(tl s, hd s)
    pre len s > 0;

    minrec: seq of nat * nat -> nat
    minrec(s, min) ==
            if s = []
            then min
            else if hd s < min
            then minrec(tl s, hd s)
            else minrec(tl s, min);

请注意，这不会尝试在比较中使用成对的值，因此没有“tl tl seq”表达式等。以下测试再次使用 VDMJ：

> p seq_min([])
Error 4055: Precondition failure: pre_seq_min in 'DEFAULT' (z.vdm) at line 5:15
Stopped in 'DEFAULT' (z.vdm) at line 5:15
5:      pre len s > 0;
>
> p seq_min([1])
= 1
Executed in 0.002 secs.
> p seq_min([2,1])
= 1
Executed in 0.014 secs.
> p seq_min([5,2,3,7,6,9,8,3,5,5,2,7,2])
= 2
Executed in 0.004 secs.
>

【讨论】：