Verification and Refinement Theory of Action Inheritance for Concurrent Objects

Abstract

<p>Lime is an action-based concurrent object-oriented programming language. Lime treats concurrency and object-orientation as a single concern and encapsulates concurrent features within objects. In Lime objects, concurrency is expressed with guarded methods and actions. Inheritance is a characteristic feature of object-oriented programming languages. Lime supports inheritance of methods. In this thesis we extend class inheritance in Lime to include inheritance of actions. This ensures that autonomous behavior of the class is also inherited. Class inheritance also aids in verification and refinement of classes. We establish class refinement rules for class inheritance. When these rules are satisfied, the subclass is a subtype as well as a refinement of the parent class. Lime uses modules as a means to define classes in terms of action systems. In our research, we extend the modules to support class inheritance. In this extended form, class modularization is useful for verification and class refinement. Concurrent object-oriented programming languages are affected by the Inheritance Anomaly - a conflict between inheritance and concurrency. We show that Lime's support for atomicity of methods and actions up to method calls allows our model of classes' inheritance to avoid the problem of the Inheritance Anomaly.</p>