Search

Refactoring engines may have overly strong preconditions preventing developers from applying useful transformations. We find that 32 percent of the Eclipse and JRRT test suites are concerned with detecting overly strong preconditions. In general, developers manually write test cases, which is costly and error prone. Our previous technique detects overly strong preconditions using differential testing. However, it needs at least two refactoring engines. In this work, we propose a technique to detect overly strong preconditions in refactoring engines without needing reference implementations. We automatically generate programs and attempt to refactor them. For each rejected transformation, we attempt to apply it again after disabling the preconditions that lead the refactoring engine to reject the transformation. If it applies a behavior preserving transformation, we consider the disabled preconditions overly strong. We evaluate 10 refactorings of Eclipse and JRRT by generating 154,040 programs. We find 15 overly strong preconditions in Eclipse and 15 in JRRT. Our technique detects 11 bugs that our previous technique cannot detect while missing 5 bugs. We evaluate the technique by replacing the programs generated by JDolly with the input programs of Eclipse and JRRT test suites. Our technique detects 14 overly strong preconditions in Eclipse and 4 in JRRT.

Context: It is common to consider Alloy signatures or UML classes as data types that have a canonical fixed interpretation: the elements of the type correspond to terms recursively generated by the type constructors. However, these language constructs resemble data types but, strictly, they are not. Objective: In this article, we propose an idiom to specify data types in Alloy. Method: We compare our approach to others in the context of checking data refinement using the Alloy Analyzer tool. Results: Some previous studies do not include the generation axiom and may perform unsound analysis. Other studies recommend some optimizations to overcome a limitation in the Alloy Analyzer tool. Conclusion: The problem is not related to the tool but the way data types must be represented in Alloy. This study shows the importance of using automated analyses to test translation between different language constructs.

Industry widely uses unstructured merge tools that rely on textual analysis to detect and resolve conflicts between code contributions. Semistructured merge tools go further by partially exploring the syntactic structure of code artifacts, and, as a consequence, obtaining significant merge accuracy gains for Java-like languages. To understand whether semistructured merge and the observed gains generalize to other kinds of languages, we implement two semistructured merge tools for JavaScript, and compare them to an unstructured tool. We find that current semistructured merge algorithms and frameworks are not directly applicable for scripting languages like JavaScript. By adapting the algorithms, and studying 10,345 merge scenarios from 50 JavaScript projects on GitHub, we find evidence that our JavaScript tools report fewer spurious conflicts than unstructured merge, without compromising the correctness of the merging process. The gains, however, are much smaller than the ones observed for Java-like languages, suggesting that semistructured merge advantages might be limited for languages that allow both commutative and non-commutative declarations at the same syntactic level.

Context: Maintaining software families is not a trivial task. Developers commonly introduce bugs when they do not consider existing dependencies among features. When such implementations share program elements, such as variables and functions, inadvertently using these elements may result in bugs. In this context, previous work focuses only on the occurrence of intraprocedural dependencies, that is, when features share program elements within a function. But at the same time, we still lack studies investigating dependencies that transcend the boundaries of a function, since these cases might cause bugs as well.Objective: This work assesses to what extent feature dependencies exist in actual software families, answering research questions regarding the occurrence of intraprocedural, global, and interprocedural dependencies and their characteristics.Method: We perform an empirical study covering 40 software families of different domains and sizes. We use a variability-aware parser to analyze families source code while retaining all variability information.Results: Intraprocedural and interprocedural feature dependencies are common in the families we analyze: more than half of functions with preprocessor directives have intraprocedural dependencies, while over a quarter of all functions have interprocedural dependencies. The median depth of interprocedural dependencies is 9.Conclusion: Given these dependencies are rather common, there is a need for tools and techniques to raise developers awareness in order to minimize or avoid problems when maintaining code in the presence of such dependencies. Problems regarding interprocedural dependencies with high depths might be harder to detect and fix.

Currently most developers have to apply manual steps and use test suites to improve confidence that transformations applied to object-oriented (OO) and aspect-oriented (AO) programs are correct. However, it is not simple to do manual reasoning, due to the nontrivial semantics of OO and AO languages. Moreover, most refactoring implementations contain a number of bugs since it is difficult to establish all conditions required for a transformation to be behavior preserving. In this article, we propose a tool (SafeRefactorImpact) that analyzes the transformation and generates tests only for the methods impacted by a transformation identified by our change impact analyzer (Safira). We compare SafeRefactorImpact with our previous tool (SafeRefactor) with respect to correctness, performance, number of methods passed to the automatic test suite generator, change coverage, and number of relevant tests generated in 45 transformations. SafeRefactorImpact identifies behavioral changes undetected by SafeRefactor. Moreover, it reduces the number of methods passed to the test suite generator. Finally, SafeRefactorImpact has a better change coverage in larger subjects, and generates more relevant tests than SafeRefactor.

HighlightsWe present a design rule specification language for aspect-oriented systems.We explore its benefits to supporting the modular development of classes and aspects.We discuss how our language improves crosscutting modularity without breaking class modularity.We present a Compiler for LSD and AspectJ (COLA), a tool to automate design rules checking.We evaluate it using a real case study and compare it with other approaches. Aspect-oriented programming is known as a technique for modularizing crosscutting concerns. However, constructs aimed to support crosscutting modularity might actually break class modularity. As a consequence, class developers face changeability, parallel development and comprehensibility problems, because they must be aware of aspects whenever they develop or maintain a class. At the same time, aspects are vulnerable to changes in classes, since there is no contract specifying the points of interaction amongst these elements. These problems can be mitigated by using adequate design rules between classes and aspects. We present a design rule specification language and explore its benefits since the initial phases of the development process, specially with the aim of supporting modular development of classes and aspects. We discuss how our language improves crosscutting modularity without breaking class modularity. We evaluate it using a real case study and compare it with other approaches.

A software product line (SPL) encodes a potentially large variety of software products as variants of some common code base. Up until now, re-using traditional static analyses for SPLs was virtually intractable, as it required programmers to generate and analyze all products individually. In this work, however, we show how an important class of existing inter-procedural static analyses can be transparently lifted to SPLs. Without requiring programmers to change a single line of code, our approach SPLLIFT automatically converts any analysis formulated for traditional programs within the popular IFDS framework for inter-procedural, finite, distributive, subset problems to an SPL-aware analysis formulated in the IDE framework, a well-known extension to IFDS. Using a full implementation based on Heros, Soot, CIDE and JavaBDD, we show that with SPLLIFT one can reuse IFDS-based analyses without changing a single line of code. Through experiments using three static analyses applied to four Java-based product lines, we were able to show that our approach produces correct results and outperforms the traditional approach by several orders of magnitude.

Mistakes made when implementing or specifying the models of a Software Product Line (SPL) can result in ill-formed products - the safe composition problem. Such problem can hinder productivity and it might be hard to detect, since SPLs can have thousands of products. In this article, we propose a language independent approach for verifying safe composition of SPLs with dedicated Configuration Knowledge models. We translate feature model and Configuration Knowledge into propositional logic and use the Alloy Analyzer to perform the verification. To provide evidence for the generality of our approach, we instantiate this approach in different compositional settings. We deal with different kinds of assets such as use case scenarios and Eclipse RCP components. We analyze both the code and the requirements for a larger scale SPL, finding problems that affect thousands of products in minutes. Moreover, our evaluation suggests that the analysis time grows linearly with respect to the number of products in the analyzed SPLs.

To safely evolve a software product line, it is important to have a notion of product line refinement that assures behavior preservation of the original product line products. So in this article we present a language independent theory of product line refinement, establishing refinement properties that justify stepwise and compositional product line evolution. Moreover, we instantiate our theory with the formalization of specific languages for typical product lines artifacts, and then introduce and prove soundness of a number of associated product line refinement transformation templates. These templates can be used to reason about specific product lines and as a basis to derive comprehensive product line refinement catalogues.

Refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics, not guaranteeing the absence of type errors or semantic changes. Consequently, developers using refactoring tools must rely on compilation and tests to ensure type-correctness and semantics preservation, respectively, which may not be satisfactory to critical software development. In this paper, we formalize a static semantics for Alloy, which is a formal object-oriented modeling language, and encode it in Prototype Verification System (PVS). The static semantics' formalization can be useful for specifying and proving that transformations in general (not only refactorings) do not introduce type errors, for instance, as we show here.

Object cloning is demanded by the prototype design pattern, copy-on-write strategy, some graph transformations, and many other scenarios. We have been developing a static analysis tool that clones objects frequently. In that context, issues related to performance, memory usage, and code maintainability might arise. Traditional deep cloning with dynamic allocation, reflection, and serialization, have not fulfilled those requirements. Thus, we developed novel implementations of lazy cloning with dynamic proxies and aspect-oriented programming (AOP). We defined benchmarks based on real workload to quantitatively assess the benefits of each implementation. AOP was chosen since it better harmonizes performance, memory usage and code maintainability. It was 88% faster than serialization, consumed 9 times less memory than reflection, and required 25 times less modifications on source code than dynamic allocation. In summary, we believe that the results can be extrapolated to broader contexts helping developers to make evidence-based decisions when object cloning is needed.

A product line refinement theory formalizes safe evolution in terms of a refinement notion, which does not rely on particular languages for the elements that constitute a product line. Based on this theory, we can derive refinement templates to support safe evolution scenarios. To do so, we need to provide formalizations for particular languages, to specify and prove the templates. Without a systematic approach, this leads to many similar templates and thus repetitive verification tasks. We investigate and explore similarities between these concrete languages, which ultimately results in a product line of theories, where different languages correspond to features, and products correspond to theory instantiations. This also leads to specifying refinement templates at a higher abstraction level, which, in the long run, reduces the specification and proof effort, and also provides the benefits of reusing such templates for additional languages plugged into the theory. We use the Prototype Verification System to encode and prove soundness of the theories and their instantiations. Moreover, we also use the refinement theory to reason about safe evolution of the proposed product line of theories.

This paper presents an extension of the Haskell programming language with the objective of improving modularization of functional programs. This extension, AspectH, extends Haskell with aspect oriented concepts. AspectH implements Aspect-Oriented Programming (AOP) through pointcuts and advice, like in AspectJ, and was designed to be used in Haskell programs that use monads. Keywords: Aspect-oriented programming, functional programming, Haskell, monads, Este artigo apresenta uma extensão da linguagem de programação Haskell com o objetivo de melhorar a modularização de programas funcionais. Esta extensão, chamada AspectH, estende Haskell com conceitos de orientação a aspectos. AspectH implementa Programação Orientada a Aspectos (AOP) através de pointcuts e advice, como em AspectJ, e foi projetada para atuar em programas Haskell que utilizam mônadas. Palavras-chave: Programação orientada a aspectos, programação funcional, Haskell, mônadas.

We present algebraic laws for a language similar to a subset of sequential Java that includes inheritance, recursive classes, dynamic binding, access control, type tests and casts, assignment, but no sharing. These laws are proved sound with respect to a weakest precondition semantics. We also show that they are complete in the sense that they are sufficient to reduce an arbitrary program to a normal form substantially close to an imperative program; the remaining object-oriented constructs could be further eliminated if our language had recursive records. This suggests that our laws are expressive enough to formally derive behaviour preserving program transformations; we illustrate that through the derivation of provably-correct refactorings.

This paper proposes modeling laws for Alloy, a formal object-oriented modeling language. These laws are important not only to define the axiomatic semantics of Alloy but also to guide and formalize popular software development practices. In particular, these laws can be used to formaly refactor specifications. As an example, we formally refactor a specification for Java types.

This paper reports our experience using AspectJ, a general-purpose aspect-oriented extension to Java, to implement distribution and persistence aspects in a web-based information system. This system was originally implemented in Java and restructured with AspectJ. Our main contribution is to show that AspectJ is useful for implementing several persistence and distribution concerns in the application considered, and other similar applications. We have also identified a few drawbacks in the language and suggest some minor modifications that could significantly improve similar implementations. Despite the drawbacks, we argue that the AspectJ implementation is superior to the pure Java implementation. Some of the aspects implemented in our experiment are abstract and constitute a simple aspect framework. The other aspects are application specific but we suggest that different implementations might follow the same aspect pattern. The framework and the pattern allow us to propose architecture-specific guidelines that provide practical advice for both restructuring and implementing certain kinds of persistent and distributed applications with AspectJ.

In this chapter we review essential concepts we explore in this work. Firstly, we review software families and software product lines, since the problem we address here is critical in these contexts. We show the basic concepts and then move towards conditional compilation with preprocessors, a widely used mechanism to implement features in industrial practice. Despite the widespread usage, conditional compilation has several drawbacks. We then present the Virtual Separation of Concerns (VSoC) approach, which can minimize some of these drawbacks. In this work, we intend to address the lack of feature modularity. Thus, we need to catch dependencies between features and inform developers about them. To do so, we rely on dataflow analyses, the last topic we review in this chapter.

In Software Product Lines (SPL), we can bind reusable features to compose a product at different times, which in general are static or dynamic. The former allows customizability without any overhead at runtime. On the other hand, the latter allows feature activation or deactivation while running the application with the cost of performance and memory consumption. To implement features, we might use aspect-oriented programming (AOP), in which aspects enable a clear separation between base code and variable code. In this context, recent work provides AspectJ-based idioms to implement flexible feature binding. However, we identified some design deficiencies. Thus, to solve the issues of these idioms, we incrementally create three new AspectJ-based idioms. Moreover, to evaluate our new idioms, we quantitatively analyze them with respect to code cloning, scattering, tangling, and size by means of software metrics. Besides that, we qualitatively discuss our new idioms in terms of code reusability, changeability, and instrumentation overhead.

Aspect-oriented programming (AOP) is a popular technique for modularizing crosscutting concerns. However, constructs aimed at supporting crosscutting modularity may break class modularity. For example, to understand a method call may require a whole-program analysis to determine what advice applies and what that advice does. Moreover, in AspectJ, advice is coupled to the parts of the program advised, the base code, so the meaning of advice may change when the base code changes. Such coupling also hinders parallel development between base code and aspects. We propose some simple modifications to the design of crosscut programming interfaces (XPIs) to include expressive design rule specifications. We call our form of XPIs crosscutting programming interfaces with design rules (XPIDRs). The XPIDR-based approach, by design, supports modular runtime checking and parallel development by decoupling aspects from base code. We also show how XPIDRs allow specification of interesting control flow effects, such as when advice does (or does not) proceed. We have implemented XPIDRs as a simple contract extension to AspectJ. Since XPIDRs do not require any new AspectJ constructs, they can be adopted easily by the AspectJ community.

When maintaining a feature in preprocessor-based Software Product Lines (SPLs), developers are susceptible to introduce problems into other features. This is possible because features eventually share elements (like variables and methods) with the maintained one. This scenario might be even worse when hiding features by using techniques like Virtual Separation of Concerns (VSoC), since developers cannot see the feature dependencies and, consequently, they become unaware of them. Emergent Interfaces was proposed to minimize this problem by capturing feature dependencies and then providing information about other features that can be impacted during a maintenance task. In this paper, we present Emergo, a tool capable of computing emergent interfaces between the feature we are maintaining and the others. Emergo relies on feature-sensitive dataflow analyses in the sense it takes features and the SPL feature model into consideration when computing the interfaces.

Software product lines (SPLs) are commonly developed using annotative approaches such as conditional compilation that come with an inherent risk of constructing erroneous products. For this reason, it is essential to be able to analyze SPLs. However, as dataflow analysis techniques are not able to deal with SPLs, developers must generate and analyze all valid methods individually, which is expensive for non-trivial SPLs. In this paper, we demonstrate how to take any standard intraprocedural dataflow analysis and automatically turn it into a feature-sensitive dataflow analysis in three different ways. All are capable of analyzing all valid methods of an SPL without having to generate all of them explicitly. We have implemented all analyses as extensions of SOOT's intraprocedural dataflow analysis framework and experimentally evaluated their performance and memory characteristics on four qualitatively different SPLs. The results indicate that the feature-sensitive analyses are on average 5.6 times faster than the brute force approach on our SPLs, and that they have different time and space tradeoffs.

During Software Product Line (SPL) maintenance tasks, Virtual Separation of Concerns (VSoC) allows the programmer to focus on one feature and hide the others. However, since features depend on each other through variables and control-flow, feature modularization is compromised since the maintenance of one feature may break another. In this context, emergent interfaces can capture dependencies between the feature we are maintaining and the others, making developers aware of dependencies. To better understand the impact of code level feature dependencies during SPL maintenance, we have investigated the following two questions: how often methods with preprocessor directives contain feature dependencies? How feature dependencies impact maintenance effort when using VSoC and emergent interfaces? Answering the former is important for assessing how often we may face feature dependency problems. Answering the latter is important to better understand to what extent emergent interfaces complement VSoC during maintenance tasks. To answer them, we analyze 43 SPLs of different domains, size, and languages. The data we collect from them complement previous work on preprocessor usage. They reveal that the feature dependencies we consider in this paper are reasonably common in practice; and that emergent interfaces can reduce maintenance effort during the SPL maintenance tasks we regard here.

Maintainability of a software product line depends on the possibility to modularize its variations, often expressed in terms of optionally selected features. Conventional modularization techniques bind variations either statically or dynamically, but ideally it should be possible to flexibly choose between both. In this paper, we propose improved solutions for modularizing and flexibly binding varying features in form of idioms in aspect-oriented languages AspectJ and CaesarJ. We evaluate the idioms qualitatively by discussing their advantages and deficiencies and quantitatively by means of metrics.

Object models provide abstract information about software structure, but their maintenance is difficult after refactoring takes place. In Model-Driven Development (MDD), effective transferral of model refactoring changes to programs is problematic, especially if these programs are subject to developer manipulation. Consequently, code-driven approaches end up being adopted. We formalize a theory of synchronizers, which are sequences of behavior-preserving program transformations. This theory makes use of invariant-based refactoring, the key idea behind synchronizers. We also establish and prove a soundness theorem for synchronizers. By uncovering the formal requirements for correct refactoring synchronization, the proved properties point out issues - regarding consistency, refactoring automation and quality - that recur in several MDD settings that employ object models.

To safely derive and evolve a software product line, it is important to have a notion of product line refactoring and its underlying refinement notion, which assures behavior preservation. In this paper we present a general theory of product line refinement by extending a previous formalization with explicit interfaces between our theory and the different languages that can be used to create product line artifacts. More important, we establish product line refinement properties that justify stepwise and compositional product line development and evolution.

Summary form only given. The extractive and the reactive software product line (SPL) adoption strategies involve, respectively, bootstrapping existing products into a SPL and extending an existing SPL to encompass another product. In both cases, product line refactorings are useful to guide the SPL derivation process by extracting product variations and appropriately structuring them. They also help to assure the safety of the whole process by preserving SPL configurability. In this context, we describe FLiP, which is a suite of tools implemented as Eclipse plugins and has been designed and tested in the context of mobile game SPLs.

Concurrent programs are essential in the development of Web based information systems. The wide dissemination of these systems increased the need for methods to create correct and efficient concurrent programs, which are usually difficult to implement and test. This paper presents guidelines to improve the concurrent control structure of object-oriented software using aspect-oriented programming through AspectJ based on an existent object-oriented concurrency control implementation method. We have defined a simple aspect framework that can be extended to implement concurrency control in applications complying with a software architecture presented in this paper. The framework comprises a set of reusable aspects useful for modularizing concurrency control.

Modularization of crosscutting concerns is the main benefit provided by aspect-oriented constructs. In order to rigorously assess the overall impact of this kind of modularization, we use design structure matrixes (DSMs) to analyze different versions (OO and AO) of a system. This is supported by the concept of semantic dependencies between classes and aspects, leading to a more faithful notion of coupling for AO systems. We also show how design rules can make those dependencies explicit and, consequently, yield a more modular design.

Adoption strategies for Software Product Lines (SPL) frequently involve bootstrapping existing products into a SPL and extending an existing SPL to encompass another product. One way to do that is to use program refactorings. However, the traditional notion of refactoring does not handle appropriately feature models (FM), nor transformations involving multiple instances of the same SPL. For instance, it is not desirable to apply a refactoring into a SPL and reduce its configurability. In this paper, we extend the traditional notion of refactoring to an SPL context. Besides refactoring programs, FMs must also be refactored. We present a set of sound refactorings for FMs. We evaluate this extended refactoring definition for SPL in a real case study in the mobile games domain.

In this chapter, we present algebraic laws for a language similar to a subset of sequential Java that includes inheritance, recursive classes, dynamic binding, access control, type tests and casts, assignment, but no sharing. We show that these laws are complete, in the sense that they are sufficient to reduce any program to a normal form substantially close to an imperative program: classes and inheritance are used only to preserve the notion of subtyping; all classes have empty bodies, except the object class, which collects all the attributes moved up from all its subclasses. Methods are also eliminated by first resolving dynamic binding, and then in-lining their bodies in place of the calls. This suggests that our laws are expressive enough to formally derive behaviour preserving program transformations; this is illustrated through the derivation of refactorings.

Both model and program refactorings are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics. In this paper, we propose guidelines on how to rigorously prove model refactorings for Alloy, a formal object-oriented modeling language. We use the Prototype Verification System (PVS) to specify and prove the soundness of the transformations. Proposing refactorings in this way can facilitate not only design, but also improve the quality of refactoring tools.

Applying refactorings to object-oriented systems usually affects source code and its associated models, involving complex maintenance efforts to keep those artifacts up to date. Most projects abandon design information in the form of models early in the life cycle, as their sustentation becomes extremely expensive. We propose a formal approach to consistently refactor systems in a model-driven manner. The refactoring applied to the model is linked to a sequence of behavior-preserving transformations that automatically refactor the underlying source code, based on structural properties from the model that must be implemented by the program. As a consequence, sound program refactoring can be accomplished without developer intervention, based only on the applied model transformations. Also, the refactored source code is consistent with the refactored model. Model information can be additionally used to improve refactoring automation, as more powerful transformations can be mechanized.

In this article we introduce a comprehensive set of algebraic laws for ROOL, a language similar to sequential Java but with a copy semantics. We present a few laws of commands, but focus on the object-oriented features of the language. We show that this set of laws is complete in the sense that it is sufficient to reduce an arbitrary ROOL program to a normal form expressed in a restricted subset of the ROOL operators. We also propose a law for data refinement that generalises the technique from traditional modules to class hierarchies. Together, these laws are expressive enough to derive more elaborate rules that can be useful, for example, to formalize object-oriented design practices; this is illustrated through the systematic derivation of a refactoring from the proposed laws.

We propose a mechanised strategy to turn an infinite CSPZ process (formed of CSP and Z constructs) into one suitable for model checking. This strategy integrates two theories which allow us to consider the infiniteness of CSPZ as two separate problems: data independence for handling the behavioural aspect and abstract interpretation for handling the data structure aspect. A distinguishing feature of our approach to abstract interpretation is the generation of the abstract domains based on a symbolic execution of the process.

In this work we propose an extension of the MooZ formal specification language with support for parameterized packages. This enhances MooZ’s capabilities for software reuse and maintenance in the large. We discuss several design issues for MooZ’s structuring mechanisms: the distinction between inheritance and subtyping, values and objects, vertical and horizontal composition, packages and classes. We also analyse the impact of our design decisions on software reuse.

This article describes informally a method for translating formal, model-based specifications into functional prototypes. Such prototypes can be used to validate software system specifications in the very early stages of the design process. We show how to translate the executable subset of the Vienna Development Method (VDM) language into Lazy ML, establishing the translation schemes and requirements needed for an automated translation process. Here we are not concerned with implicit specifications, but indicate, in places, what has to be done for such specifications to be automatically translated into a functional program. A small example—part of a translation system from VDM to LML—gives the reader a good idea of the power of the approach.