Спецификация 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

Выглядит действительно рекурсивно, не так ли?Книга «Структуры данных с использованием C и C ++», написанная Йедиджей Лангсам, Моше Дж. Огенштейном и Аароном М. Тененбаумом, второе издание, получила хорошее обсуждение.Первоначально он показывает

пострадиционное условное [0] == a;makerational [1] == b;

, затем обсуждается тот факт, что 1/2 и 2/4 следует считать равными, и пересматривается определение.Я думаю, что это может быть прочитано что-то вроде: Элемент [0] результирующих RATIONAL умножить на b должен равняться элементу [1] результирующих RATIONAL умноженных на a

Answer 2

Если вы знаете, что такое рациональное число , а именно одно целое число, деленное на другое, то нетрудно выяснить это обозначение.

Я никогда не видел его раньше, но изИз свойств рациональных чисел (дробей) ясно, что индексация в квадратных скобках предназначена для представления в виде вектора из двух целых чисел.

Тогда в обычной математической записи

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

Cheers &НТН,