ogp-notes

Introduction: Topic of the course

This is the course text for the course “Object-oriented programming” at KU Leuven, Belgium. This course introduces students to three related topics:

Modular programming is the principal method by which software engineers manage the complexity of the task of building, maintaining, and evolving large software systems. Modular programming means decomposing software systems into a number of modules, which may be developed, understood, verified, and evolved independently from, and in parallel with, other modules. By enabling this independent evolution, the principle allows building, maintaining and evolving software systems that are much larger and more complex than would otherwise be possible.

A module may interact with another module by invoking the latter’s operations. (We then say the former is a client module of the latter.) To make independent development possible, modular programming requires a clear and abstract specification of the API offered by a module to its client modules, that is, of the syntax and semantics (behavior) of the operations defined by the module for use by clients. Each module must then be implemented such that it complies with its API specification. Additionally, this correctness must only depend on the specifications, not the implementations, of the modules whose program elements it uses. Good specifications of module APIs are widely recognized as essential in software engineering, especially for important, long-lived APIs between separately developed modules.

For example, consider a student using an HP laptop running the Google Chrome web browser on Microsoft Windows to remotely attend a course via Blackboard Inc.’s bbcollab.com website. The software system running on this laptop consists of (at least) four modules:

From time to time, Blackboard Inc., Google, Microsoft, and HP, independently and in parallel, develop new versions of their module and deploy them to the student’s laptop. If the student’s laptop keeps working correctly, this is thanks to the fact that the APIs between these modules have been specified clearly and carefully.

As shown by this example, the principle of modular programming is extremely general. Specifically, its relevance is not restricted to object-oriented programming or high-level languages like Java. Nevertheless, this course covers modular software development in the context of OOP and particularly Java. Both the OOP model and Java include principles (like encapsulation) and features (like static types) that facilitate modularity and defining APIs. Additionally, both OOP and the Java community traditionally attach great value to modularity and specification of APIs.

The focus of this course will be on how to design and clearly define the syntax and semantics of module APIs. For defining the syntax of APIs, we will make use of Java’s strong support for this, particularly its strong static typing, and its support for encapsulation: the compiler and virtual machine (Java’s execution environment) together enforce that a module is accessed only through its official API, and that the correct number and types of arguments are passed to each API call. However, besides precisely defining the syntax of APIs, it is crucial to also precisely define a module API’s semantics (meaning), in terms of the behavior generated by API calls. Therefore, in this course, we put a strong emphasis on how to write clear and comprehensive documentation for APIs.

For the sake of clarity and precision, we will supplement informal documentation with formal specifications. These express properties of APIs using a well-defined syntax that can be given a precise meaning. Although such formal specifications are not standard (even in large projects that attach great value to modularity), we believe it is useful to expose students to them, because they encourage students to be fully precise, think about corner cases and reason rigorously about correctness. Because there is no widely accepted formalism, we use a minimal one designed specifically for this course.

About the author Bart Jacobs obtained his PhD in Computer Science at KU Leuven in 2007, and is a Professor at KU Leuven since 2010. He has authored, with others, papers on modular formal verification of safety and liveness properties of imperative programs involving programming language features such as dynamic binding or function pointers, fine-grained concurrency, exceptions, unloadable modules, I/O, and synchronization using condition variables, channels, or busy waiting, among others. Furthermore, he is the lead developer of the VeriFast tool for modular formal verification of C and Java programs.