Because somebody was confused about ADTs and classes. ---
Depending on the programming language logic, ADTs can be defined in algebraic style (equations in which the terms are made by functional compositions and applications) or state based specifications (as in Hoare triples {Precondition}, program {Postcondition},).
The prototypical ADT example is a Stack , which as an abstract data type, can be specified algebraically, as:
functions:
Empty : -> Stack.adt /* (constructor, where Stack is the name of the module , ) */
isempty : Stack.adt -> bool
push : (Stack.adt x E) -> Stack.adt
pop : Stack.adt -> Stack.adt /* partially defined */
top : Stack.adt -> E
axioms:
isempty(Empty) = true
isempty(push(s,e)) = false
top(push(s,e)) = e
pop(push(s,e)) = s
Or can be defined using Hoare triples :
{true}, s := Stack.Create; { isempty(s) },
{true}, push(s, e); { ! isempty(s) },
{s = s0 }, push(s,e); pop(s) { s=s0 },
{true}, push(s,e); e1 := top(s) { e=e1 },