Refactoring is a well known software development technique that can bring several bene?ts to aspect- oriented applications by allowing developers to introduce aspects to an existing object-oriented program as well as changing the aspect-oriented program itself. Aspect-oriented developers have been identifying common transformations, but they sometimes lack support for assuring that the transformations preserve behavior and are indeed refactorings. This book focuses on that problem and introduces AspectJ programming laws that can be used to derive or create behavior preserving transformations (refactorings) for a subset of this language. Programming laws de?ne equivalence between two programs, given that some conditions are met. By applying and composing these laws, one can show that a transformation involving AspectJ is a refactoring. This book shows how these laws can be used to derive several refactorings proposed in other literature. This helps to more precisely specify the preconditions and code changes associated with those refactorings, and gives more con?dence that they will preserve behavior.