有谁知道我可以去完全理解这个符号的语法的任何教程?
/* 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] ]