集/序列求和运算符? [英] Set/sequence summation operator?

问题描述

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

如果我想用标准逻辑求和，那只是ΣS(SO上没有MathJax，所以我不能很好地格式化它).

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

什么是VDM等效项?我在语言参考的数字/设置"部分看不到任何内容.

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

推荐答案

没有标准的库函数可以执行此操作(尽管应该这样做).您将使用简单的递归函数对集合求和:

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;

"let"从集合中选择一个任意元素，然后将其添加到余数的总和中.该措施表明，递归总是处理较小的集合.

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.

这篇关于集/序列求和运算符?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！