Aspect-oriented programming and modular reasoning

Proceedings. 27th International Conference on Software Engineering, 2005. ICSE 2005. ◽

10.1145/1062455.1062482 ◽

2005 ◽

Cited By ~ 55

Author(s):

Gregor Kiczales ◽

Mira Mezini

Keyword(s):

Aspect Oriented Programming ◽

Modular Reasoning

Download Full-text

MRI: Modular reasoning about interference in incremental programming

Journal of Functional Programming ◽

10.1017/s0956796812000354 ◽

2012 ◽

Vol 22 (6) ◽

pp. 797-852 ◽

Cited By ~ 7

Author(s):

BRUNO C. D. S. OLIVEIRA ◽

TOM SCHRIJVERS ◽

WILLIAM R. COOK

Keyword(s):

Side Effects ◽

Object Oriented ◽

Object Oriented Programming ◽

Hard Problem ◽

Aspect Oriented Programming ◽

Modular Reasoning ◽

Data Flows ◽

Tightly Coupled ◽

Algebraic Laws ◽

Program Components

AbstractIncremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include Object-oriented programming inheritance, aspect-oriented programming advice, and feature-oriented programming. A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity, and reasoning with algebraic laws about effectful operations. These techniques enable MRI in the presence of side effects. MRI formally captures harmlessness, a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques.

Download Full-text

An Algebraic Approach for the Specification and the Verification of Aspect-Oriented Systems

Advances in Systems Analysis, Software Engineering, and High Performance Computing - Handbook of Research on Emerging Advancements and Technologies in Software Engineering ◽

10.4018/978-1-4666-6026-7.ch008 ◽

2014 ◽

pp. 148-174

Author(s):

Arsène Sabas ◽

Subash Shankar ◽

Virginie Wiels ◽

John-Jules Ch. Meyer ◽

Michel Boyer

Keyword(s):

Algebraic Approach ◽

Object Oriented ◽

Entire System ◽

Aspect Oriented Programming ◽

Modular Reasoning ◽

Object Oriented Technology ◽

Open Issue ◽

Specification And Verification ◽

Use Category ◽

Over Time

Aspect-Oriented (AO) Technology is a post-object-oriented technology used to overcome limitations of Object-Oriented (OO) Technology, such as the cross-cutting concern problem. Aspect-Oriented Programming (AOP) also offers modularity and traceability benefits. Yet, reasoning, specification, and verification of AO systems present unique challenges, especially as such systems evolve over time. Consequently, formal modular reasoning of such systems is highly attractive as it enables tractable evolution, otherwise necessitating that the entire system be re-examined each time a component is changed or is added. The aspect interactions problem is also an open issue in the AOP area. To deal with this problem, the authors choose to use Category Theory (CT) and Algebraic Specification (AS) techniques. In this chapter, the authors present an aspect-oriented specification and verification approach. The approach is expressive and allows for formal modular reasoning.

Download Full-text