Оператор суммирования наборов / последовательностей?

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

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

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

Источник

2 ответа

Решение

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

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" выбирает произвольный элемент из набора, а затем прибавляет его к сумме остатка. Мера говорит, что рекурсия всегда имеет дело с меньшими наборами.

Источник

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

sum(S)

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

Источник
Другие вопросы по тегам