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.