ADT规范
有谁知道我可以去哪里完全理解这种表示法的语法的教程吗？
/* 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] ]
Does any one know any tutorial where I can go to fully understand the syntax of this notation?
/* 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] ]
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
如果您知道有理数是什么，即一个整数除以另一个整数，那么就不难理解该表示法。
我以前从未见过它，但从有理数（分数）的属性来看，很明显，方括号索引用于表示为两个整数的向量。
然后，用普通的数学符号，
Cheers &哈，
If you know what a rational number is, namely one integer divided by another, then it's not difficult to figure out that notation.
I have never seen it before, but from the properties of rational numbers (fractions) it's clear that the square brackets indexing is for a representation as a vector of two integers.
Then, in ordinary math notation,
Cheers & hth,
makerational 看起来确实是递归的，不是吗！
《使用 C 和 C++ 的数据结构，Yedidyah Langsam、Moshe J. Augenstein 和 Aaron M. Tenenbaum 所著，第二版》一书有很好的讨论。它最初显示后
置条件 makerational[0] == a;
makerational[1] == b;
然后讨论了 1/2 和 2/4 应被视为相等的事实，并修改了定义。我认为它可以读成这样：
RATIONAL 乘以 b 的结果的 [0] 元素必须等于 RATIONAL 乘以 a 的结果的 [1] 元素
makerational looks really recursive, doesn't it!
The book "Data Structures Using C and C++, by Yedidyah Langsam, Moshe J. Augenstein, and Aaron M. Tenenbaum, second edition" has a good discussion. It initially shows
postcondition makerational[0] == a;
makerational[1] == b;
then it discusses the fact that 1/2 and 2/4 should be considered equal, and revises the definition. I think it could be read something like :
The [0] element of the resulting RATIONAL times b must equal the [1] element of the resulting RATIONAL times a