SHF: Small: Collaborative Research: Balancing Expressiveness and Modular Reasoning for Aspect-oriented Programming

软件系统的复杂性将持续增长，并深入渗透到社会的关键基础设施中。这些系统的复杂性超过了现有模块化机制的极限，对可靠性的要求也越来越严格。因此，开发新的关注点分离（SoC）技术对于提高软件的可靠性和可维护性至关重要。隐式调用（II）和面向方面（AO）编程语言为关注点分离提供了相关但不同的机制。建议的工作包括改进II和AO语言的模块化和推理机制的基础和实际努力，这是两种语言长期面临的挑战。通过简化新的关注点分离技术的采用，解决这些挑战具有显著提高软件质量的潜力。该项目将使用实验语言托勒密进行，它融合了II和AO的思想。托勒密显式地宣布了事件，这些事件定义在称为“事件类型”的接口中。事件类型有助于分离关注点，并将建议与其所建议的代码解耦。事件类型声明还提供了指定通知的位置。事件的明确声明允许对托勒密计划的正确性进行仔细推理的可能性，因为可以用传统的方式对计划中没有事件的部分进行推理。该项目旨在通过开发一种正式的规范语言和验证技术来研究推理。该方法基于灰盒（“模型程序”）规范的思想，如在JML和细化演算中发现的那样。有一些已知的技术可以对具有模型程序规范的抽象的使用进行推理，该项目将把这些技术应用于托勒密。智力上的优点是在处理托勒密的表达，宣布事件和那些导致一个建议进行。对这些情况的现有推理技术的直接适应似乎需要整个程序分析，这对于模块化和可伸缩的验证通常是不可取的。该项目还旨在调查托勒密及其规范体系的效用和有效性。将进行软件演化分析，以研究竞争的面向方面、隐式调用和开源项目的托勒密实现抵御变化的能力。展示托勒密相对于II和AO语言的优势将有助于软件设计人员决定采用高级的关注点分离机制。

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.