В нотации Z, как определить операцию деления для целых чисел

Question

Мне было интересно узнать, использовал ли кто-нибудь здесь даже "Z-нотацию" в профессиональной среде. Просто любопытно узнать некоторые общеизвестные приложения Z или ваше приложение.

Для тех, кто не знаком: http://staff.washington.edu/jon/z/z-examples.html

Я хочу знать, "В нотации Z, как определить операцию деления для целых чисел"

Answer 1

Целочисленное деление уже является частью математического инструментария Z:

a \div b

(См. Руководство Z по М. Spivey, глава 4.4. Числа и конечность)