VDMSL Recursive function minimum value of sequence

Question

I think this should be relatively straightforward, was wondering if anyone knew how to answer this:

Define a recursive function seq-min : N+ -> N which returns the smallest value in a sequence of natural numbers.

I was thinking something along the lines of...

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)

Thanks for any help!

Answer 1

Here is a slightly different approach, using a single function:

    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;

This has the advantage that it is short and intuitive (and a single function). Specifications can be very clear when they are written as a set of "patterns" in a cases expression like this, as each case is explicitly "explained".

Answer 2

Something like that might work, but it is quite hard to follow - and we are writing a specification, so it helps if it is clear. The following was my first thought. It cheats slightly by using two functions, but I hope it is relatively clear:

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

Note that this does not try to use pairs of values in the comparison, so there is no "tl tl seq" expression etc. The following tests are with VDMJ again:

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