For example, a stack has push/pop operations that follow a Last-In-First-Out rule, and can be concretely implemented using either a list or an array.
ADTs are a theoretical concept, used in formal semantics and program verification and, less strictly, in the design and analysis of algorithms, data structures, and software systems.
For example, in modular programming, the module declares procedures that correspond to the ADT operations, often with comments that describe the constraints.
[1] ADTs were first proposed by Barbara Liskov and Stephen N. Zilles in 1974, as part of the development of the CLU language.
[2] Algebraic specification was an important subject of research in CS around 1980 and almost a synonym for abstract data types at that time.
In the spirit of functional programming, each state of an abstract data structure is a separate entity or value.
To underscore this view, it is customary to say that the operations are executed or applied, rather than evaluated, similar to the imperative style often used when describing abstract algorithms.
In that case, one needs additional axioms that specify how much memory each ADT instance uses, as a function of its state, and how much of it is returned to the pool by free.
The definition of an ADT often restricts the stored value(s) for its instances, to members of a specific set X called the range of those variables.
As in programming languages, such restrictions may simplify the description and analysis of algorithms, and improve its readability.
Alexander Stepanov, designer of the C++ Standard Template Library, included complexity guarantees in the STL specification, arguing: The reason for introducing the notion of abstract data types was to allow interchangeable software modules.
In the operational semantics, fetch(V) is a procedure that returns the current value in the location V, and store(V, x) is a procedure with void return type that stores the value x in the location V. The constraints are described informally as that reads are consistent with writes.
As in many programming languages, the operation store(V, x) is often written V ← x (or some similar notation), and fetch(V) is implied whenever a variable V is used in a context where a value is required.
There are some algorithms whose efficiency depends on the assumption that such a fetch is legal, and returns some arbitrary value in the variable's range.
In the axiomatic semantics, creating the initial stack is a "trivial" operation, and always returns the same distinguished state.
Here it is implicitly assumed that operations on a stack instance do not modify the state of any other ADT instance, including other stacks; that is: A more involved example is the Boom hierarchy of the binary tree, list, bag and set abstract data types.
Within each of the equivalence classes implied by the chosen subset of equations, it has to yield the same result for all of its members.
AGDTs provide the advantages of ADTs with facilities to build graphical objects in a structured way.
This means each ADT instance or state is represented by some concrete data type or data structure, and for each abstract operation there is a corresponding procedure or function, and these implemented procedures satisfy the ADT's specifications and axioms up to some standard.
For example, integers may be specified as an ADT, defined by the distinguished values 0 and 1, the operations of addition, subtraction, multiplication, division (with care for division by zero), comparison, etc., behaving according to the familiar mathematical axioms in abstract algebra such as associativity, commutativity, and so on.
Nonetheless, for many purposes, the user can ignore these infidelities and simply use the implementation as if it were the abstract data type.
This provides a form of abstraction or encapsulation, and gives a great deal of flexibility when using ADT objects in different situations.
The implementation of the module—namely, the bodies of the procedures and the concrete data structure used—can then be hidden from most clients of the module.
Modern object-oriented languages, such as C++ and Java, support a form of abstract data types.
The module's interface typically declares the constructors as ordinary procedures, and most of the other ADT operations as methods of that class.
Many modern programming languages, such as C++ and Java, come with standard libraries that implement numerous ADTs in this style.
The specification of some programming languages is intentionally vague about the representation of certain built-in data types, defining only the operations that can be done on them.
Examples are the arrays in many scripting languages, such as Awk, Lua, and Perl, which can be regarded as an implementation of the abstract list.
The OBJ family of programming languages for instance allows defining equations for specification and rewriting to run them.
The implementation may be arbitrarily inefficient, since the formal definition of the ADT, above, does not specify how much space the stack may use, nor how long each operation should take.