VDM-SL - function接受一组整数并返回相同的集合

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}。