Essential AOP: The a calculus
Essential AOP: The a calculus
复制标题
基本 AOP：微积分
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Mario Südholt
中科院分区：
文献类型：
--
作者：
B. D. Fraine;Erik Ernst;Mario Südholt
面向方面的编程（AOP）产生了有趣的语言设计，但也需要澄清的临时语义。我们用一块积极对AOP进行建模的阐明做出了贡献，这比现有形式化更简单，更笼统。在AOP中，建议可以拦截方法调用，并继续执行暂停的呼叫。继续是一种临时机制，只能在咨询机构内部使用。例如，通配符，许多尖端机制也缺乏规律性。我们使用一流的封闭来建模，并将复杂性从点刻度转移到普通面向对象的代码。通常认为两个众所周知的命名类别，即呼叫和执行。我们正式暴露了它们的差异，并解决了相关的声音问题。我们的演算包括类型范围，这是显式类型变量的直观而简洁的替代方案，允许建议与截距方法相比多态性。我们使用微积分参数来涵盖其他功能的广泛设计空间的类型安全性。类型的声音已在COQ中验证。
Aspect-oriented programming (AOP) has produced interesting language designs, but also ad hoc semantics that needs clarification. We contribute to this clarification with a calculus that models essential AOP, both simpler and more general than existing formalizations. In AOP, advice may intercept method invocations, and proceed executes the suspended call. Proceed is an ad hoc mechanism, only usable inside advice bodies. Many pointcut mechanisms, for example, wildcards, also lack regularity. We model proceed using first-class closures, and shift complexity from pointcuts to ordinary object-oriented code. Two well-known pointcut categories, call and execution, are commonly considered similar. We formally expose their differences, and resolve the associated soundness problem. Our calculus includes type ranges, an intuitive and concise alternative to explicit type variables that allows advice to be polymorphic over intercepted methods. We use calculus parameters to cover type safety for a wide design space of other features. Type soundness is verified in Coq.