vdm++ - 集合/序列求和运算符？

Question

我有一套，S = { 1, 2, 3, 4, 5 }.

如果我想用标准逻辑总结它，它只是 ∑S（SO 上没有 MathJax，所以我不能很好地格式化这个）。

什么是 VDM 等价物？我在语言参考的数字/集合部分看不到任何内容。

Answer 1

这应该有效：

sum(S)

但是你可以很容易地找到它。

Answer 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”从集合中选择一个任意元素，然后将其添加到余数的总和中。该度量表示递归始终处理较小的集合。