Software systems are poised to keep growing in complexity and permeate deeper into the critical infrastructures of society. The complexity of these systems is exceeding the limits of existing modularization mechanisms and reliability requirements are becoming stringent. Development of new separation of concerns (SoC) techniques is thus vital to make software more reliable and maintainable. Implicit invocation (II) and aspect-oriented (AO) programming languages provide related but distinct mechanisms for separation of concerns. The proposed work encompasses fundamental and practical efforts to improve modularization and reasoning mechanisms for II and AO languages, which is a long standing challenge for both kinds of languages. Addressing these challenges has the potential to significantly improve the quality of software by easing the adoption of new separation of concerns techniques.
The project will proceed using the experimental language, Ptolemy, which blends both II and AO ideas. Ptolemy has explicitly announced events, which are defined in interfaces called "event types". Event types help separate concerns and decouple advice from the code it advises. Event type declarations also offer a place to specify advice. The explicit announcement of events allows the possibility of careful reasoning about correctness of Ptolemy programs, since it is possible to reason about parts of the program where there are no events in a conventional manner. The project aims to investigate reasoning by developing a formal specification language and verification technique. The approach is based on the idea of greybox ("model program'') specifications, as found in JML and the refinement calculus. There are known techniques for reasoning about uses of abstractions that have model program specifications, and the project will apply these to Ptolemy. The intellectual merit is in the treatment of expressions in Ptolemy that announce events and those that cause an advice to proceed. A straightforward adaptation of existing reasoning techniques to these cases appears to require a whole program analysis, which is generally not desirable for modular and scalable verification. The project also aims to investigate the utility and effectiveness of Ptolemy and its specification system. A software evolution analysis will be conducted to study the ability of competing aspect-oriented, implicit invocation, and Ptolemy implementations of open source projects to withstand change. Showing Ptolemy's benefits over II and AO languages will help software designers in deciding on advanced mechanisms for separation of concerns.
Software systems are essential elements of modern society -- they improve upon many natural and artificial processes that ultimately benefits the society and the individual. The production of software systems has come a long way in the last six decades. With improved tools and techniques increasing useful software systems and software-enabled devices are being constructed and deployed. Software systems of 21st century are very complex because their goals mirror complexity that is inherent to the natural or artificial process that the software is modeling. In software construction, a major technique for managing this complexity is "separation of concerns". Basic idea is to provide software developers the ability to understand variousfacets of the software in isolation. This allows developers to maintain intellectual controlover increasing complexity. During the last five decades invention and refinement of separation of concerns techniques have allowed productivity of software developers to keep pace with increasing complexity. Software systems are poised to keep growing in complexity and permeate deeper into the critical infrastructures of society. The complexity of these systems is once again exceeding the limits of existing modularization mechanisms and reliability requirements are becoming stringent. Development of new separation of concerns techniques is thus vital to make software more reliable and maintainable. Implicit invocation (II) and aspect-oriented (AO) programming languages provide related but distinct mechanisms for separation of concerns. This research encompassed fundamental and practical efforts to improve modularization and reasoning mechanisms for II and AO languages, which was a long standing challenge for both kinds of languages. Addressing these challenges has the potential to significantly improve the quality of software by easing the adoption of new separation of concerns techniques. The project proceeded by studying a language, Ptolemy, which blends both II and AO ideas.Ptolemy has explicitly announced events, which are defined in interfaces called "event types". Event types help separate concerns and decouple advice from the code it advises. Event typedeclarations also offer a place to specify advice. The explicit announcement of events allows the possibility of careful reasoning about correctness of Ptolemy programs, since it is possible to reason about parts of the program where there are no events in a conventional manner.The project investigated reasoning by developing a formal specification language and verification technique. The approach is based on the idea of greybox ("model program'')specifications, as found in the JML language and the refinement calculus. There are known techniques for reasoning about uses of abstractions that have model program specifications,and the project applied these to Ptolemy to produce the novel notion of translucid contracts. The intellectual merit was in the treatment of expressions in Ptolemy that announce events and those that cause an advice to proceed. A straightforward adaptation of existing reasoning techniques to these cases required a whole program analysis, which is generally not desirable for modular and scalable verification. The project also investigated the utility and effectiveness of Ptolemy and its specification system. A software evolution analysis was conducted to study the ability of competing aspect-oriented, implicit invocation, and Ptolemy implementations of open source projects to withstand change. Showing Ptolemy's benefits over II and AO languages will help software designers in deciding on advanced mechanisms for separation of concerns.
