Задать / Последовательность оператора суммирования?

Question

У меня есть набор, S = { 1, 2, 3, 4, 5 }.

Если бы я хотел суммировать это в стандартных логах c, это просто ∑S (нет MathJax на SO, поэтому я не могу отформатировать это красиво).

Что такое эквивалент VDM? Я не вижу ничего в разделе чисел / наборов ссылки на язык.

Answer 1

Для этого нет стандартной библиотечной функции (хотя, возможно, она и должна быть). Вы суммируете набор с помощью простой рекурсивной функции:

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;

«Let» выбирает произвольный элемент из набора, а затем добавляет его к сумме остатка. Мера говорит, что рекурсия всегда имеет дело с меньшими наборами.

Answer 2

Это должно работать:

sum(S)

Но вы можете найти это очень легко.