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 }