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

干杯&心连心，

Answer 2

makerational看起来真的递归的，不是吗！ “Yedidyah Langsam，Moshe J. Augenstein和Aaron M. Tenenbaum，第二版”的书籍“数据结构使用C和C++”有很好的讨论。它最初显示为

postcondition makerational [0] == a; makerational [1] == b;

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