Advanced Aspects of Object-Oriented Programming

Lecture Slides

Contents of the Lecture

• 1.1 Overview
• 1.2 Formal and Notational Foundations

• 2.1 Concepts of Object-Oriented Programming
  • 2.1.1 Basic Concepts
  • 2.1.2 Linguistic Concepts
  • 2.1.3 Pragmatic Aspects
• 2.2 Semantics of Object-Oriented Languages
  • 2.2.1 Introduction
  • 2.2.2 Operational Semantics of a Sublanguage of Java
  • 2.2.3 About the Theory of Structural Operational Semantics Definitions
• 2.3 Properties of Object-Oriented Programs
  • 2.3.1 Assertions
  • 2.3.2 Statement Specifications
  • 2.3.3 Trace Properties
  • 2.3.4 Interface Properties
  • 2.3.5 Other Properties
• 2.4 Modularity and Encapsulation
  • 2.4.1 Modularity and Modular Specification
  • 2.4.2 Encapsulation and Interface Generation
  • 2.4.3 Realization of Encapsulation

• 3.1 Introduction
  • 3.1.1 Type Information and their Static and Dynamic Checking
  • 3.1.2 Type Safety
• 3.2 Parametric Type Systems and Virtual Classes
  • 3.2.1 Parametric Type Systems
  • 3.2.2 Virtual Types
• 3.3 Type Systems for Structuring the Object Store
  • 3.3.1 Encapsulation at Package Level: Confined Types
  • 3.3.2 Other Approaches to Structuring
• 3.4 Extended Static Checking
  • 3.4.1 General Aspects of ESP
  • 3.4.2 The Tool ESC/Java

• 4.1 Specification of Types
  • 4.1.1 Lightweight Specifications
  • 4.1.2 Specification of Single Objects
  • 4.1.3 Specification with Abstract Variables
  • 4.1.4 Specification of Interacting Objects
• 4.2 Conformance of Subtypes
• 4.3 Modules and Modularity
  • 4.3.1 Properties on Module Level
  • 4.3.2 Modular Specification

• 5.1 Techniques for Verification
• 5.2 Verification by Proof

Preconditions:

Continuating Literature:

• Arnd Poetzsch-Heffter:
  Konzepte objektorientierter Programmierung, Springer-Verlag, 2000.
• Kim B. Bruce:
  Foundations of Object-Oriented Languages. Types and Semantics. MIT Press, 2002.
• Sophia Drossopoulou, Susan Eisenbach:
  Java is Type Safe - Probably. ECOOP, 1997 (LNCS 1241).
• Tobias Nipkow, David von Oheimb:
  Java light is Type Safe - Definitely Principles of Programming Languages, 1998.
• Atsushi Igarashi, Benjamin Pierce, Philip Wadler:
  Featherweight Java: A Minimal Core Calculus for Java and GJ. OOPSLA, 1999.
• Gilad Bracha, Martin Odersky, David Stoutamire, Philip Wadler:
  Making the future safe for the past: Adding Genericity to the Java Programming Language. OOPSLA, 1998.
• Kresten Krab Thorup:
  Genericity in Java with Virtual Types. ECOOP, 1997.
• Kim B. Bruce, Martin Odersky, Philip Wadler:
  A statically safe alternative to virtual types. ECOOP, 1998.
• Boris Bokowski, Jan Vitek:
  Confined Types. OOPSLA, 1999.
• Paulo Sergio Almeida:
  Balloon Types: Controlling Sharing of State in Data Types. ECOOP, 1997.
• David G. Clarke, John M. Potter, James Noble:
  Ownership Types for Flexible Alias Protection. OOPSLA, 1998.
• David G. Clarke, John M. Potter, James Noble:
  Simple Ownership Types for Object Containment. ECOOP, 2001.
• Peter Müller, Arnd Poetzsch-Heffter:
  A Type System for Controlling Representation Exposure in Java. Formal Techniques for Java Programs, 2000.
• K. Rustan M. Leino, Greg Nelson:
  Data abstraction and information hiding. Transactions on Programming Languages and Systems 24(5): pages 491-553, 2002.
• Barbara H. Liskov, Jeannette M. Wing:
  A Behavioral Notion of Subtyping. Transactions on Programming Languages and Systems 16(6), pages 1811-1841, 1994.