Theory behind object oriented programming

Question

Alonzo Church's lambda calculus is the mathematical theory behind functional languages. Has object oriented programming some formal theory ?

Answer 1

I'd check out wikipedia's page on OO http://en.wikipedia.org/wiki/Object-oriented_programming It's got the principles and fundamentals and history.

My understanding is that it was an evolutionary progression of features and ideas in a variety of languages that finally came together with the push in the 90's for GUI's going mainstream. But i could be horribly wrong :-D

Edit: What's even more interesting is that people still argue about "what makes an OO language OO"..i'm not sure the feature set is even generally agreed upon that defines an OO language.

Answer 2

OOP is a bit of a mixed bag of features that various languages implement in slightly different ways. There is no single formal definition of OOP but a number of people have tried to describe OOP based on the common features of languages that claim to be object oriented. From Wikipedia:

Benjamin Cuire Pierce and some other researchers view as futile any attempt to distill OOP to a minimal set of features. He nonetheless identifies fundamental features that support the OOP programming style in most object-oriented languages:

• Dynamic dispatch – when a method is invoked on an object, the object itself determines what code gets executed by looking up the method at run time in a table associated with the object. This feature distinguishes an object from an abstract data type (or module), which has a fixed (static) implementation of the operations for all instances. It is a programming methodology that gives modular component development while at the same time being very efficient.
• Encapsulation (or multi-methods, in which case the state is kept separate)
• Subtype polymorphism
• object inheritance (or delegation)
• Open recursion – a special variable (syntactically it may be a keyword), usually called this or self, that allows a method body to invoke another method body of the same object. This variable is late-bound; it allows a method defined in one class to invoke another method that is defined later, in some subclass thereof.

Answer 3

One formal definition I've run into for strongly defining and constraining subtyping is the Liskov Substitution Principle. It is certainly not all of object-oriented programming, but yet it might serve as a link into the formal foundations in development.