Suad Alagić Object- Oriented Technology Object-Oriented Technology Suad Alagic´ Object-Oriented Technology 123 SuadAlagic´ ComputerScienceProfessor Portland,Maine,USA Publications:http://dblp.uni-trier.de/pers/hd/a/Alagic:Suad Website:https://sites.google.com/site/suadalagicme/ ISBN978-3-319-20441-3 ISBN978-3-319-20442-0 (eBook) DOI10.1007/978-3-319-20442-0 LibraryofCongressControlNumber:2015944088 SpringerChamHeidelbergNewYorkDordrechtLondon ©SpringerInternationalPublishingSwitzerland2015 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartof thematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation, broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionorinformation storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodology nowknownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsor theeditorsgiveawarranty,expressorimplied,withrespecttothematerialcontainedhereinorforany errorsoromissionsthatmayhavebeenmade. Printedonacid-freepaper SpringerInternationalPublishingAGSwitzerlandispartofSpringerScience+BusinessMedia(www. springer.com) For Adrian,Evan,Lucas,andDario Preface Thecoreideaofthisbookisthatobject-orientedtechnologyisagenerictechnology whose various technical aspects could be presented in a unified and consistent framework. This applies to both practical and formal aspects of object-oriented technology. The approach in the book is based on typed technologies. The core notions fit mainstream object-oriented languages such as Java and C#. However, perhaps the most distinctive feature of this book is that it is based on object-oriented con- straints(assertions),theirspecificationandverification.Object-orientedconstraints apply to specification and verification of object-oriented programs, specifica- tion of the object-oriented virtual platform, more advanced concurrent models, database integrity constraints, and object-oriented transactions, their specification andverification. In Chap.1, we define the key notions of typed object-oriented technology: the notions of types, objects, classes, messages, and methods. This is followed by the notions of inheritance and subtyping and their formal and pragmatic properties. Staticanddynamicbindingasitappliestomessagesandmethodsisthendiscussed. Parametrictypesareessentialformoderntypedobject-orientedtechnologies.They are given due attention through a detailed analysis of various issues related to parametrictypes. A distinctive view in this book is that types are preferably equipped with assertions.AssertionsarethetopicofChap.2.Thischapterfirstspecifiesthebasic reasoningrulessuchasthosethatapplytoassignments,conditionalstatements,and loops.Loopinvariantsandaverificationtechniqueforprovingterminationarethen discussed. Object-oriented assertions: method preconditions and postconditions, and class invariants are discussed in detail. Finally, we revisit the notion of subtypinginthepresenceofassertionsandexplaintheallimportantcompatibility requirementsforclassescalledbehavioralsubtyping.Thischapteralsoshowshow assertions are specified in a sample application that makes use of a practical assertionspecificationandverificationtool. The formal basis in this book for types and constraints had an impact on the notation used to present code samples that are based on Java, C#, assertion, and vii viii Preface data languages. Although these code samples are close to the source languages, they are more conceptual and based on notation that is closer to the standard mathematicalnotation.Thisproducesaconsistentframeworkforbothcodesamples and their formal aspects expressed by constraints. The correspondence with the sourcenotationisimmediate. In Chap.3, we describe a modern environment that supports typed object- oriented technology. The components of this environment include reflection, the actualobject-orientedvirtualmachine,andsupportforpersistentobjects.Reflection is presented following the initial Java specifications that are more suitable for explanationofcoreconceptsunlikethemorerecentrevisions.Moderntypedobject- oriented languages such as Java or C# run on an object-oriented virtual machine. Our presentation is an abstraction of the existing very low-level specifications of object-oriented virtual machines. A distinctive feature of the presentation is the use of assertions to define the semantics of the basic operations. An object- orientedplatformshouldsupportpersistentobjects,i.e.,objectswithlonglifetimes. This chapter also presents persistent models and mechanisms such as orthogonal persistenceandserializability. In Chap.1, we present the basic rules of object-oriented type systems in a mostly informal manner. However, type systems have an elaborate formal theory. In Chap. 4, we show how some of the elements of type theory apply to an object-oriented programming language. We first explain the basic typing rules for statementssuchasassignment,conditionals,andloops,aswellasforexpressions. Then we focus on the rules of object-oriented type systems that govern classes, inheritance, subtyping, and messages. These static typing rules are followed by dynamic type checking rules that mainstream object-oriented languages have, and the formal rules for parametric types. In addition, we present static and dynamic typing rules that apply to reflection. Finally, we show what kind of problems violation of type safe rules can cause. We take a well-known paradigm of type erasurethatwasthebasisofthetechniqueforextendingJavawithparametrictypes. This paradigm is provably incorrect as demonstrated by a variety of cases of type violationpresentedinthischapter. Concurrentobject-orientedmodelsarediscussedinChap.5.Wefirstpresentthe modelofconcurrentthreadsofexecution.Then,weexplainthebasicmechanisms forsynchronizingconcurrentaccessofmultiplethreadstoobjectsonthecommon heap. We discuss the relationship between synchronization and inheritance, and the relationship between serialization and synchronization. We demonstrate what the implications are of synchronized versus unsynchronized executions. Then, we introduceamoregeneralconcurrentanddistributedmodelbasedonasynchronous messages. The basis of this model is the fact that messages may be viewed as objects.Inthisnewframework,itisnaturaltodefineformallytherulesofbehavioral subtyping.Finally,weintroduceaverygeneralmodelofconcurrentactiveobjects, eachequippedwithitsownvirtualmachine.Ambientsofsuchobjectsarediscussed aswell. Object-oriented database technology (the topic of Chap.6) addresses the lim- itations of relational and extended relational technologies in managing complex Preface ix objects that exhibit complex behavior. Object-oriented database technology is also addressing the problem of the mismatch between the dominating software technology,whichisobject-oriented,andthedominatingdatabasetechnologythat is relational, or object-relational at best. This specifically applies to the so-called “impedancemismatch”betweendataandprogramminglanguages.Wefirstdiscuss thebasicfeaturesofobject-orienteddefinitionandquerylanguages.Welookatthe mostimportantobject-orienteddatabasetechnologies.Weexplainthecorefeatures ofthosetechnologiesthatincludedatabasecollectionclasses,interfacingdatabases from an object-oriented programming language, and object-oriented transactions. We also revisit the typing issues for persistent collections. The core features of a specific current technology and its application are presented as well. Finally, we discuss a critical limitation of all object-oriented and other database technologies: inability to specify and enforce very general database integrity constraints. We presentanobject-orienteddatabaseparadigmbasedonsuchgeneralconstraints. In Chap.7, we show how two critical formal notions in this book: types and constraints, apply to two significant practical problems. The first problem is specification of database type systems in a formal manner. The second problem is specification and verification of object-oriented transactions. Database systems are typically not based on a formally specified type system. This leads to non- trivial problems that we demonstrate in this chapter. We consider a type system required by object-oriented database systems and establish a collection of the required formal rules showing the typing problems in object-oriented database languages.Thischapteralsoaddressesanotherkeyfeatureofdatabasetechnologies: transactions. Unlike other approaches, object-oriented schemas and transactions are in our approach equipped with integrity constraints expressed in an object- orientedassertionlanguage.Thisisfollowedbyobject-orientedconsistencyissues. The presentation is based on a sample object-oriented schema equipped with very generalintegrityconstraintsandsampletransactions.Therelationshipbetweenthe integrity constraints and queries is discussed, as well as inheritance for object- oriented schemas equipped with constraints. An essential issue of the role of dynamicversusstaticcheckingofconstraintsisalsoaddressedinthischapter. Portland,Maine,USA SuadAlagic´ Acknowledgements The author is grateful to two software engineers, Russell Gillen and Thomas Keschl, his former graduate students, for their numerous valuable comments that significantlyimprovedthemanuscript.