vdm-sl - VDM-SL - 函数接受一组整数并返回一个相同的集合

Question

尝试一个接受整数并返回我想出的整数的非负值的函数

Abs : int -> nat
Abs(num) == if num < 0
        then -num
        else num;

现在我正在尝试创建另一个函数，它接受一组整数并返回一个相同的集合，其中每个元素都是原始值的绝对值。

PositiveSet : set of int -> set of int

请帮忙：（

Answer 1

您将需要某种集合理解——“x 的绝对值集合，其中 x 取自集合 S”。签名将是“seq of int -> seq of nat”，因为结果总是自然数。

一个小点：返回的集合可能不是“相同的”，因为它可能包含比输入更少的元素。例如。{-1, 0, 1} 将更改为 {0, 1}。