Спецификация 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 выглядит действительно рекурсивной, не правда ли! Книга «Структуры данных, использующие C и C++, Yedidyah Langsam, Moshe J. Augenstein и Aaron M. Tenenbaum, второе издание» имеет хорошее обсуждение. Первоначально он показывает

postcondition makerational [0] == a; создание [1] == b;

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