formal-methodsz-notation

Z notation specification to modify content of a set

Let's say I have a set:

S: Id X Counter

Id: \nat

Counter: \nat

Need help to define an operation filter which takes in two parameters, x:\nat and y:\nat which I can apply to S. This function will match on the first parameter with \exists a \in S @ first(a) = x and then reduce second(a) with y. If the value is less than or equal to zero, a should be removed from the set S, otherwise (first(a), second(a) - y) should replace a.

If the above is indecipherable, just please give me any example definition that operates over a set and modifies it.

Thanks.

Solution

  • Your set of pairs S of natural numbers is a Z relation between natural numbers. Let's give the set of all such relations a name:

    natrel == ℕ ↔ ℕ

    Since the filter function will only modify some part of S, it is convenient to describe that separately.

    The modify operation produces for a given pair (x, y) of arguments and a relation S the set of maplets a ↦ b − y satisfying your description:

    As a Z "axiomatic description" it is:

    │   
│   modify : (ℕ × ℕ) → (natrel → natrel)
│   
├───
│   
│   ∀ x, y : ℕ; S : natrel ⦁ 
│     modify (x, y) S =
│       { a, b : ℕ | a ↦ b ∈ S ∧ a = x ∧ b > y ⦁ a ↦ b − y }
│

    Note that modify (x, y) S may well be empty if there are no such maplets in S.

    Deletion of a maplet a ↦ b ∈ S where b is too small is modeled simply by excluding it in the set comprehension.

    Now the filter operation is easy to define:

    │   
│   filter : (ℕ × ℕ) → (natrel → natrel)
│   
├───
│   
│   ∀ x, y : ℕ; S : natrel ⦁ 
│     (filter (x, y) S) = ({x} ⩤ S) ∪ (modify (x, y) S)
│

    So the result of filter (x, y) S is a set union of the unchanged part of S on the left hand side with the maplets given by modify (x, y) S on the right hand side: