Как указать математическое выражение, используя спецификацию Z?

Question

Как я могу указать математическое выражение, используя Z обозначения? Я думаю, что свободные типы подходят для этой ситуации, потому что выражения имеют рекурсивный характер. пожалуйста, учтите, что в нашем выражении могут быть скобки и переменные. и только ( +, -, /, *) разрешено. например: A + 2 * ( 3 - B) / 4

Помогите мне, пожалуйста...

Answer 1

Вам нужно использовать аксиоматическое определение: определение объекта ограничено условиями.

Для этого в zet указана схема. Который

| Declaration
------------------------------
| Predicate
|
|

Приведен рекурсивный пример:

[ИМЯ ПОЛЬЗОВАТЕЛЯ] - уже определенный тип.

Для данного имени пользователя и последовательности имен пользователей (N1 -> USERNAME) возвращается число, в котором указанное имя пользователя появляется в последовательности.

|-occurs- USERNAME X seq USERNAME → N //here you define the input and what is returned.
---------------------------------------
|∀ u: USERNAME, s: seq USERNAME then
|s = < > => occurs(u,s) = 0
|s ≠ < > and head(s) = u => occurs(u,s) = 1+occurs(u,tail(s))
|s ≠ < > and head(s) ≠ u => occurs(u,s) = occurs(u,tail(s))