specifications - 如何使用 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))