c++ - 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

如果您知道什么是有理数，即一个整数除以另一个整数，那么就不难找出这个符号。

我以前从未见过它，但从有理数（分数）的性质来看，很明显方括号索引是用于表示为两个整数的向量。

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

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))

干杯&hth，

Answer 2

makerational 看起来真的是递归的，不是吗！“Data Structures Using C and C++, by Yedidyah Langsam, Moshe J. Augenstein, and Aaron M. Tenenbaum, second edition”一书有很好的讨论。它最初显示

后置条件 [0] == a; 制造理性[1] == b;

然后讨论了 1/2 和 2/4 应该被视为相等的事实，并修改了定义。我认为它可以这样读：所得 RATIONAL 乘以 b 的 [0] 元素必须等于所得 RATIONAL 乘以 a 的 [1] 元素