Unity-inspired object-oriented concurrent system development

Abstract

The design of correct software remains difficult, especially when dealing with concurrency. The primary goal of the research presented here is to devise a pragmatic software development method which  aids the software designer in producing reliable software,  is scalable,  is understandable,  follows a unified approach towards software development (is applicable to different implementation architectures),  promotes reuse,  has seamless transitions between the software development phases,  guarantees general availability and minimises developmental resources. The two main characteristics of the proposed new development method are captured in its name, viz. Single Location Object-Oriented Programming (SLOOP) . It is an object-oriented method, but its computational model is that of a set of statements that execute infinitely often and in any order. A program with such a computational model is called a Single Location Program (SLP). A UNITY program can also be classified as a Single Location Program. In the UNITY theory of programming it was demonstrated how this computational model could simplify correctness reasoning, particularly for concurrent systems. It is this simplification, together with the structuring and reuse features of object-orientation, that is leveraged in the SLOOP method to produce a mechanism whereby ordinary software practitioners can take advantage of the benefits of a more rigorous approach towards software development without requiring an in-depth understanding of the underlying mathematics. The following features of the SLOOP method contribute towards achieving the above goals:  its computational model (it simplifies correctness reasoning, thereby promoting understandability and scalability, and also facilitates designs that are independent of the target implementation architectures),  its object-oriented nature (apart from promoting reuse of frameworks, design patterns and classes, the SLOOP method provides the necessary mechanisms to facilitate reuse of correctness properties, correctness arguments as well as mappings to implementation architectures),  its emphasis on correctness reasoning throughout the software development life cycle (its "constructive approach" aids reliability and seamlessness),  the unique way in which the correctness properties can be specified, reused and reasoned about (this contributes towards understandability and scalability),  the checklist of useful correctness properties that is provided (this promotes reliability),  the incorporation of existing notations into the SLOOP syntax (this guarantees general availability, minimises developmental resources and aids understandability). The main contribution of this thesis is that it presents a unique way of incorporating the SLP computational model into an object-oriented method with the specific aim of simplifying informal correctness reasoning and promoting reuse. The notation used for the specification of correctness properties facilitates reuse of correctness properties, ensures the integrity of these specifications and allows one to specify correctness properties at a higher level of abstraction. The SLOOP method offers a unique way of modelling concurrency in object-oriented systems (via its parallel methods), which takes full advantage of the encapsulation and inheritance features of object-orientation. The issues surrounding mappings to implementation architectures are addressed, showing how even mappings can be reused. Finally, the general applicability of the SLOOP method is demonstrated.