Set/sequence summation operator?

Question

I have a set, S = { 1, 2, 3, 4, 5 }.

If I wanted to sum this in standard logic it's just ∑S (no MathJax on SO so I can't format this nicely).

What's the VDM equivalent? I don't see anything in the numerics/sets section of the language reference.

Answer 1

There isn't a standard library function to do this (though perhaps there should be). You would sum a set with a simple recursive function:

sum: set of nat +> nat
sum(s) ==
    if s = {}
    then 0
    else let e in set s in
        e + sum(s \ {e})
measure card s;

The "let" selects an arbitrary element from the set, and then add that to the sum of the remainder. The measure says that the recursion always deals with smaller sets.

Answer 2

This should work:

sum(S)

But you could find this very easily.