1

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

定义一个递归函数 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)

谢谢你的帮助！

4

2 回答 2

1

类似的事情可能会奏效，但很难遵循 - 我们正在编写规范，所以如果它很清楚，它会有所帮助。以下是我的第一个想法。它通过使用两个函数稍微作弊，但我希望它相对清楚：

    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.
>
于 2014-06-03T11:36:28.803 回答
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;

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

于 2014-06-03T13:10:39.577 回答