Return highest or lowest value Z notation , formal method

Question

I am new to Z notation,

Lets say I have a function f defined as X |--> Y , where X is string and Y is number.

How can I get highest Y value in this function? Does 'loop' exist in formal method so I can solve it using loop?

I know there is recursion in Z notation, but based on the material provided, I only found it apply in multiset or bag, can it apply in function?

Any extra reference application of 'loop' or recursion application will be appreciated. Sorry for my English.

Answer 1

You can just use the predefined function max that takes a set of integers as input and returns the maximum number. The input values here are the range (the set of all values) of the function:

max(ran(f))

Please note that the maximum is not defined for empty sets.

Regarding your question about recursion or loops: You can actually define a function recursively but I think your question aims more at a way to compute something. This is not easily expressed in Z and this is IMO a good thing because it is used for specifications and it is not a programming language. Even if there wouldn't be a max or ran function, you could still specify the number m you are looking for by:

\exists s:String @ (s,m):f /\
  \forall s2:String, i2:Z @ (s2,i2):f ==> i2 <= m

("m is a value of f, belonging to an s and all other values i2 of f are smaller or equal")

After getting used to the style it is usually far better to understand than any programming language (except your are trying to describe an algorithm itself and not its expected outcome).#

Just for reference: An example of a recursive definition (let's call it rmax) for the maximum would consist of a base case:

\forall e:Z @ rmax({e}) = e

and a recursive case:

\forall e:Z; S:\pow(Z) @
    S \noteq {} \land
    rmax({e} \cup S) = \IF e > rmax(S) \THEN e \ELSE rmax(S)

But note that this is still not a "computation rule" of rmax because e in the second rule can be an arbitrary element of S. In more complex scenarios it might even be not obvious that the defined relation is a function at all because depending on the chosen elements different results could be computed.