Search

Abstract: Software engineering research is driven by the aim of making software development more dynamic, flexible and evolvable. Nowadays the emphasis is on the evolution of pre-existing sub-systems and component and service-based development, where often only a part of the system is totally under control of the designer, most components being remotely operated by external vendors. In this context, we tackle the following problem: given the formal specification of the (incomplete) system, say it , already built, how to characterize collaborators of to be selected, based on a given communication interface , so that a given property is satisfied. Using properties described by temporal logic formulae and systems by CCS processes, if is the formula to be satisfied by the complete system, an efficient and automatic procedure is defined to identify a formula such that, for each existing process satisfying , the process satisfies . Important features of this result are simplicity of the derived property , compared to the original one, and scalability of the verification process. Such characteristics are necessary for applying the method to both incremental design and system evolution scenarios where is already in place, and one needs to understand the specification of the functionality of the new component that should correctly interact with . Indeed, in general, finding a suitable partner for is easier than finding a complete system satisfying the global property. Moreover, in this paper it is shown how can be used also to select a set of possible candidate processes through a property-directed and structural heuristic. From the verification point of view, the description of the lacking component through a logic formula guarantees correctness of the integration with of any process that exhibits a behaviour compliant with the inferred formula. [Copyright &y& Elsevier]

Abstract: Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions. [Copyright &y& Elsevier]

Abstract: A major asset of modern systems is to dynamically reconfigure themselves to cope with failures or component updates. Nevertheless, designing such systems with off-the-shelf components is hardly feasible: components are black-boxes that can only interact with others on compatible interfaces. Part of the problem is solved through Software Adaptation techniques, which compensate mismatches between interfaces. Our approach aims at using results of Software Adaptation in order to also provide reconfiguration capabilities to black-box components. This paper first formalizes a framework that unifies behavioral adaptation and structural reconfiguration of components. This formalization is used for statically detecting whether it is possible to reconfigure a system. In a second part, we present five notions of reconfiguration: history-aware reconfiguration, future-aware reconfiguration, property-compliant reconfiguration, one-way reconfigurability, and full reconfigurability. For each of these notions, its relevant properties are presented, and they are illustrated on simple yet realistic examples. [Copyright &y& Elsevier]

Abstract: Virtual machines (VMs) are a popular target for language implementers. A long-running question in the design of virtual machines has been whether stack or register architectures can be implemented more efficiently with an interpreter. Many designers favour stack architectures since the location of operands is implicit in the stack pointer. In contrast, the operands of register machine instructions must be specified explicitly. In this paper, we present a working system for translating stack-based Java virtual machine (JVM) code to a simple register code. We describe the translation process, the complicated parts of the JVM which make translation more difficult, and the optimisations needed to eliminate copy instructions. Experimental results show that a register format reduced the number of executed instructions by 34.88%, while increasing the number of bytecode loads by an average of 44.81%. Overall, this corresponds to an increase of 2.32 loads for each dispatch removed. We believe that the high cost of dispatches makes register machines attractive even at the cost of increased loads. [Copyright &y& Elsevier]

Building upon years of evolution in object-oriented programming language design, Java has emerged as the language of choice among many educators for teaching introductory computer science. A clean, type-safe language, Java provides a garbage collected heap and a comprehensive exception-handling mechanism. However, in spite of this support, many students in introductory computer science courses still find programming to be an overwhelming source of frustration. Linguistic concerns and programming mechanics demand so much attention that deeper concepts are often postponed for later courses, leaving students in introductory courses with the mistaken impression that computer science is a shallow discipline, concerned only with transcribing ideas into code, and not with the ideas themselves.JPie is a tightly integrated programming environment for live software construction in Java. JPie treats programming as an application in its own right, providing a visual representation of class definitions and supporting direct manipulation of graphical representations of programming abstractions and constructs. Exploiting Java’s reflection mechanism, JPie supports the notion of a dynamic class that can be modified while the program is running, thereby eliminating the edit–compile–test cycle. Following years of experience using Java as the vehicle for teaching introductory computer science, we have designed JPie to provide a more natural and fluid software development process that both raises the level of abstraction and eliminates many of the common pitfalls that beginning Java programmers face. This paper studies JPie from an educational perspective. We systematically review key programming abstractions and explain how JPie supports them in ways that keep beginning programmers focused on important ideas. Our experience using JPie in an introductory computer science survey course for non-majors is briefly discussed. [Copyright &y& Elsevier]