How to understand ADT (abstract data type algebra)?

Question

I'm taking a CS course but frankly I've no idea what the lecturer is talking about in regards to abstract data type algebra. It's not something I've readily been able to find a solution for on the web and I thought maybe someone out there in the community would have greater insight or undestanding into the problem.

Stack:

isempty(createstack()) = true
isempty(push(n, s)) = false 
top(push(n, s)) = n 
pop(push(n, s)) = s

Queue:

isempty(createqueue()) = true
isempty(add(n, q)) = false
front(add(n, q)) = n, if q is empty
front(add(n, q)) = front(q), if q is not empty removefront(add(n, q)) = q,
if q is empty      removefront(add(n, q)) = add(n, removefront(q)),
if q is not empty

the notation is certainly a bit odd... what does the above mean in real terms ~ i understand the general behaviour of a queue and a stack as first in first out vs first in last out.

Answer 1

Abstract Data Types can be used to describe how the behavior of types must be without specifying an implementation. You define a type as a set of axioms or rules that describe what conditions must hold in every moment. Djikstra once said that ADTs where a very useful tool to describe the behavior of queues... But well, leaving Djikstra's known hyper-critic humor aside, I can think of at least one real application of ADT's: assertions.

Assertions allow you to specify how your type works in a formal, compilable, runnable language (as opposed to natural language documentation). In Design by contract methodoloy they are often written as predicates that must hold before or after the execution of a method (in general any operation on the type) in source language or some form of meta-language. Frameworks that support assertions (such as CodeContracts for .NET) do an automatic check that every predicate holds when it should. This way if you're own code violates one of your assertions, you know you have a bug. So in some sense it can be seen as a form of unit testing, not by specifying test cases (which would be the empirical testing methodology), but by specifying preconditions, post-conditions and invariants that your type must fit (which would be the theoretical testing methodology).

Although not used in mainstream software development, as far as I know, (checking assertions can be a performance hit) they can be used during testing.

From the purely theoretical point of view ADTs are just that, an abstraction that allows us to reason about the behavior of types regardless of their specific implementation. If you like formalisms (like I do), nothing is better that having a developer give you a list of theorems rather than a ambiguous babble describing what his code is supposed to do.

On the other hand, some alternative programming paradigms (alternative as in alternative to Object-Oriented, not as in secondary, unimportant, etc.) such as logic or functional programming are heavy based of ADTs for the types constructions. A very interesting example is the Haskell language. It gives you a hole new picture of types, inheritance and polymorphism.