VDMSL Рекурсивная функция минимальное значение последовательности

Question

Я думаю, что это должно быть относительно просто, было интересно, если бы кто-нибудь знал, как ответить на это:

Определите рекурсивную функцию 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)

Спасибо за любую помощь!

Answer 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;

Это имеет то преимущество, что оно короткое и интуитивно понятное (и единственная функция). Спецификации могут быть очень ясными, когда они написаны как набор "шаблонов" в выражении случаев, подобном этому, поскольку каждый случай явно "объясняется".

Answer 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.
>