ADT

A useful tool for specifying the logical properties of a data type is the ADT (Abstract Data Type).A data type is a collection of values and a set of operations on those values. The term “abstract data type” refers to the basic mathematical concept that defines the data type.

There are a numbers of methods for specifying an ADT.
The method that we use is semiformal and borrows heavily from C notation but extends those notations where necessary. The operations on real numbers that we define are the creation of a rational numbers from two integers, addition, multiplication, and testing for equality.
The following is an initial specification of this ADT.
/* value definitions */
abstract typedef RATIONAL;
condition RATIONAL[1]!=0;
/*operator definition*/
abstract RATIONAL make rational(a,b)
int a,b;
precondition b!=0;
post condition make rational[0]= =a;
make rational[1]= =b;

abstract RATIONAL add(a,b) /*written a+b*/
RATIONAL a,b;
Post condition add[1]= = a[1]*b[1];
add[0]= = a[0]*b[1] +b[0]*a[1];
abstract RATIONAL mult(a,b) /*written a*b*/
RATIONAL a,b;
Post condition mult[1]= = a[1]*b[1];
mult[0]= = a[0]*b[0];

abstract RATIONAL equal(a,b) /* written a= =b*/ RATIONAL a,b; Post condition equal= =(a[0]*b[1]= = a[1]*b[0]);