ADT规范

Question

有没有人知道有什么教程可以让我完全理解这个符号的语法？

/* value definition */
abstract typedef <int, int> RATIONAL;
condition RATIONAL[1] != 0;

/* Operator definitions */

abstract equal( a, b )                        /* written a == b */
RATIONAL a, b;
postcondition equal == ( a[0] * b[1] == b[0] * a[1] )

abstract RATIONAL makerational( a, b )      /*  written [a, b] */
int a, b;
precondition b != 0;
postcondition makerational[0] * b == a * makerational[1]

abstract RATIONAL add( a, b )            /* written a + b */
RATIONAL a, b;
postcondition add == [ a[0] * b[1] + b[0] * a[1], a[1] * b[1] ]

abstract RATIONAL mult( a, b )
RATIONAL a, b;
postcondition mult == [ a[0] * b[0], a[1] * b[1] ]

Answer 1

如果您知道rational number是什么，即一个整数除以另一个整数，那么就不难弄清楚这种表示法。

我以前从未见过它，但从有理数(分数)的属性可以清楚地看出，方括号索引用于表示为两个整数的向量。

然后，在普通的数学符号中，

upper( rational( a, b ) ) = a
lower( rational( a, b ) ) = b

equal( r1, r2 ) = (upper(r1)*lower(r2) eq upper(r2)*lower(r1) )
add( r1, r2 ) = rational(upper(r1)*lower(r2)+upper(r2)*lower(r1), lower(r1)*lower(r2))
mul( r1, r2 ) = rational(upper(r1)*upper(r2), lower(r1)*lower(r2))

干杯&哈，

Answer 2

makerational看起来真的很递归，不是吗！Yedidyah Langsam、MoshJ.Augenstein和AaronM.Tenenbaum合著的"Data Structures Using C and C++“一书有一个很好的讨论。它最初显示

后置条件makerational == a；makerational1 == b；

然后讨论了1/2和2/4应被视为相等的事实，并对定义进行了修正。我认为它可以这样理解:得到的有理时间b的元素必须等于得到的有理时间a的1个元素。