VDM-SL - function accepts a set of integers and returns an identical set

Question

Trying for a function that accepts an integer and returns the non-negative value of that integer which I figured out

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

now I am trying to create another function that accepts a set of integers and returns an identical set where each element is the absolute value of the original value.

PositiveSet : set of int -> set of int

please help:(

Answer 1

You would need some sort of set comprehension - "the set of absolute values of x, where x is taken from the set S". The signature would be "seq of int -> seq of nat", since the results would always be natural numbers.

One small point: the returned set might not be "identical" in the sense that it may contain fewer elements than the input. Eg. {-1, 0, 1} would change to {0, 1}.