rbFeatures: Feature-oriented programming with Ruby

Features are pieces of core functionality of a program that is relevant to particular stakeholders. Features pose dependencies and constraints among each other. These dependencies and constraints describe the possible number of variants of the program: A valid feature configuration generates a specific variant with unique behavior. Feature-Oriented Programming is used to implement features as program units. This paper introduces rbFeatures, a feature-oriented programming language implemented on top of the dynamic programming language Ruby. With rbFeatures, programmers use software product lines, variants, and features as first-class entities. This allows several runtime reflection and modification capabilities, including the extension of the product line with new features and the provision of multiple variants. The paper gives a broad overview to the implementation and application of rbFeatures. We explain how features as first-class entities are designed and implemented, and discuss how the semantics of features are carefully added to Ruby programs. We show two case studies: The expression product line, a common example in feature-oriented programming, and a web application.     

Access control in feature-oriented programming

In feature-oriented programming (FOP) a programmer decomposes a program in terms of features. Ideally, features are implemented modularly so that they can be developed in isolation. Access control mechanisms in the form of access or visibility modifiers are an important ingredient to attain feature modularity as they allow programmers to hide and expose internal details of a module’s implementation. But developers of contemporary feature-oriented languages have not considered access control mechanisms so far. The absence of a well-defined access control model for FOP breaks encapsulation of feature code and leads to unexpected program behaviors and inadvertent type errors. We raise awareness of this problem, propose three feature-oriented access modifiers, and present a corresponding access modifier model. We offer an implementation of the model on the basis of a fully-fledged feature-oriented compiler. Finally, by analyzing ten feature-oriented programs, we explore the potential of feature-oriented modifiers in FOP.     

一个经过证明的类型化汇编语言的类型检查器

编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性,包括控制流安全, 内存安全等.类型化编程语言都需要一个类型检查器来检查程序的良类型性,因此编程语言的具体实现是否能保证类型安全性,还依赖类型检查器的可靠性.本文给出一种类型化汇编语言,然后给出相应的类型检查器,并证明了此类型检查器的可靠性,从而保证经过类型检查的汇编程序的安全性.文本的所有工作,包括类型化汇编语言、类型检查器以及相关定理证明,均已在证明辅助工具Coq中实现.本文方法也可用于证明类型化高级语言的类型检查器的可靠性.     

Compositional type checking of delta-oriented software product lines

Delta-oriented programming is a compositional approach to flexibly implementing software product lines. A product line is represented by a code base and a product line declaration. The code base consists of a set of delta modules specifying modifications to object-oriented programs. A particular product in a delta-oriented product line is generated by applying the modifications contained in the suitable delta modules to the empty program. The product-line declaration provides the connection of the delta modules with the product features. This separation increases the reusability of delta modules. In this paper, we provide a foundation for compositional type checking of delta-oriented product lines of Java programs by presenting a minimal core calculus for delta-oriented programming. The calculus is equipped with a constraint-based type system that allows analyzing each delta module in isolation, such that the results of the analysis can be reused. By relying only on the analysis results for the delta modules and on the product line declaration, it is possible to establish whether all the products of the product line are well typed according to the fragment of the Java type system modeled by the calculus.     

Flow-sensitive type systems and the ambient calculus

The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code. Numerous analyses have been developed for numerous variants of that calculus. We take up the challenge of developing, in a type-based setting, a relatively precise “topology” analysis for the original version of the calculus. To compensate for the lack of “co-capabilities” (an otherwise increasingly popular extension), the analysis is flow-sensitive, with the actions of processes being summarized by “behaviors”. A subject reduction property guarantees that for a well-typed process, the location of any ambient is included in what is predicted by its type; additionally it ensures that communicating subprocesses agree on their “topic of conversation”. Based on techniques borrowed from finite automata theory, type checking of type-annotated processes is decidable (though potentially exponential).     

A Type System for the Java Bytecode Language and Verifier

The Java Virtual Machine executes bytecode programs that may have been sent from other, possibly untrusted, locations on the network. Since the transmitted code may be written by a malicious party or corrupted during network transmission, the Java Virtual Machine contains a bytecode verifier to check the code for type errors before it is run. As illustrated by reported attacks on Java run-time systems, the verifier is essential for system security. However, no formal specification of the bytecode verifier exists in the Java Virtual Machine Specification published by Sun. In this paper, we develop such a specification in the form of a type system for a subset of the bytecode language. The subset includes classes, interfaces, constructors, methods, exceptions, and bytecode subroutines. We also present a type checking algorithm and prototype bytecode verifier implementation, and we conclude by discussing other applications of this work. For example, we show how to extend our formal system to check other program properties, such as the correct use of object locks. This revised version was published online in August 2006 with corrections to the Cover Date.     

Remodularizing Java programs for improved locality of feature implementations in source code

Explicit traceability between features and source code is known to help programmers to understand and modify programs during maintenance tasks. However, the complex relations between features and their implementations are not evident from the source code of object-oriented Java programs. Consequently, the implementations of individual features are difficult to locate, comprehend, and modify in isolation. In this paper, we present a novel remodularization approach that improves the representation of features in the source code of Java programs. Both forward and reverse restructurings are supported through on-demand bidirectional restructuring between feature-oriented and object-oriented decompositions. The approach includes a feature location phase based on tracing of program execution, a feature representation phase that reallocates classes into a new package structure based on single-feature and multi-feature packages, and an annotation-based reverse transformation of code. Case studies performed on two open-source projects indicate that our approach requires relatively little manual effort and reduces tangling and scattering of feature implementations in the source code.     

Flexible feature binding in software product lines

A software product line (SPL) is a family of programs that share assets from a common code base. The programs of an SPL can be distinguished in terms of features, which represent units of program functionality that satisfy stakeholders’ requirements. The features of an SPL can be bound either statically at program compile time or dynamically at run time. Both binding times are used in SPL development and have different advantages. For example, dynamic binding provides high flexibility whereas static binding supports fine-grained customizability without any impact on performance (e.g., for use on embedded systems). However, contemporary techniques for implementing SPLs force a programmer to choose the binding time already when designing an SPL and to mix different implementation techniques when multiple binding times are needed. We present an approach that integrates static and dynamic feature binding seamlessly. It allows a programmer to implement an SPL once and to decide per feature at deployment time whether it should be bound statically or dynamically. Dynamic binding usually introduces an overhead regarding resource consumption and performance. We reduce this overhead by statically merging features that are used together into dynamic binding units. A program can be configured at run time by composing binding units on demand. We use feature models to ensure that only valid feature combinations can be selected at compile and at run time. We provide a compiler and evaluate our approach on the basis of two non-trivial SPLs.     

Quantifying structural attributes of system decompositions in 28 feature-oriented software product lines

A key idea of feature orientation is to decompose a software product line along the features it provides. Feature decomposition is orthogonal to object-oriented decomposition—it crosscuts the underlying package and class structure. It has been argued often that feature decomposition improves system structure by reducing coupling and by increasing cohesion. However, recent empirical findings suggest that this is not necessarily the case. In this exploratory, observational study, we investigate the decompositions of 28 feature-oriented software product lines into classes, features, and feature-specific class fragments. The product lines under investigation are implemented using the feature-oriented programming language Fuji. In particular, we quantify and compare the internal attributes import coupling and cohesion of the different product-line decompositions in a systematic, reproducible manner. For this purpose, we adopt three established software measures (e.g., coupling between units, CBU; internal-ratio unit dependency, IUD) as well as standard concentration statistics (e.g., Gini coefficient). In our study, we found that feature decomposition can be associated with higher levels of structural coupling in a product line than a decomposition into classes. Although coupling can be concentrated in very few features in most feature decompositions, there are not necessarily hot-spot features in all product lines. Interestingly, feature cohesion is not necessarily higher than class cohesion, whereas features are more equal in serving dependencies internally than classes of a product line. Our empirical study raises critical questions about alleged advantages of feature decomposition. At the same time, we demonstrate how our measurement approach of coupling and cohesion has potential to support static and dynamic analyses of software product lines (i.e., type checking and feature-interaction detection) by facilitating product sampling.     

A type system for logic programs

A theory for a type system for logic programs is developed which addressesthe question of well-typing, type inference, and compile-time and run-time type checking. A type is a recursively enumerable set of ground atoms, which is tuple-distributive. The association of a type to a program is intended to mean that only ground atoms that are elements of the type may be derived from the program. A declarative definition of well-typed programs is formulated, based on an intuitive approach related to the fixpoint semantics of logic programs. Whether a program is well typed is undecidable in general. We define a restricted class of types, called regular types, for which type checking is decidable. Regular unary logic programs are proposed as a specification language for regular types. An algorithm for type-checking a logic program with respect to a regular type definition is described, and its complexity is analyzed. Finally, the practicality of the type system is discussed, and some examples are shown. The type system has been implemented in FCP for FCP and is incorporated in the Logix system.     

Validated Proof-Producing Decision Procedures

A widely used technique to integrate decision procedures (DPs) with other systems is to have the DPs emit proofs of the formulas they report valid. One problem that arises is debugging the proof-producing code; it is very easy in standard programming languages to write code which produces an incorrect proof. This paper demonstrates how proof-producing DPs may be implemented in a programming language, called Rogue-Sigma-Pi (RSP), whose type system ensures that proofs are manipulated correctly. RSP combines the Rogue rewriting language and the Edinburgh Logical Framework (LF). Type-correct RSP programs are partially correct: essentially, any putative LF proof object produced by a type-correct RSP program is guaranteed to type check in LF. The paper describes a simple proof-producing combination of propositional satisfiability checking and congruence closure implemented in RSP.     

Noninterference in a predicative polymorphic calculus for access control

Polymorphic programming languages have been adapted for constructing distributed access control systems, where a program represents a proof of eligibility according to a given policy. As a security requirement, it is typically stated that the programs of such languages should satisfy noninterference. However, this property has not been defined and proven semantically. In this paper, we first propose a semantics based on Henkin models for a predicative polymorphic access control language based on lambda-calculus. A formal semantic definition of noninterference is then proposed through logical relations. We prove a type soundness theorem which states that any well-typed program of our language meets the noninterference property defined in this paper. In this way, it is guaranteed that access requests from an entity do not interfere with those from unrelated or more trusted entities.     

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.     

Static safety guarantees for a low-level multithreaded language with regions

We present the design of a formal low-level multithreaded language with advanced region-based memory management and thread synchronization primitives, where well-typed programs are memory safe and race free. In our language, regions and locks are combined in a single hierarchy and are subject to uniform ownership constraints imposed by this hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is read/write-protected, then its sub-regions inherit the same access rights. We discuss aspects of the integration and implementation of the formal language within Cyclone and evaluate the performance of code produced by the modified Cyclone compiler against highly optimized C programs using pthreads. Our results show that the performance overhead for guaranteed race freedom and memory safety is in most cases acceptable.     

Dependently typed array programs don’t go wrong

The array programming paradigm adopts multidimensional arrays as the fundamental data structures of computation. Array operations process entire arrays instead of just single elements. This makes array programs highly expressive and introduces data parallelism in a natural way. Array programming imposes non-trivial structural constraints on ranks, shapes, and element values of arrays. A prominent example where such constraints are violated are out-of-bound array accesses. Usually, such constraints are enforced by means of run time checks. Both the run time overhead inflicted by dynamic constraint checking and the uncertainty of proper program evaluation are undesirable.We propose a novel type system for array programs based on dependent types. Our type system makes dynamic constraint checks obsolete and guarantees orderly evaluation of well-typed programs. We employ integer vectors of statically unknown length to index array types. We also show how constraints on these vectors are resolved using a suitable reduction to integer scalars. Our presentation is based on a functional array calculus that captures the essence of the paradigm without the legacy and obfuscation of a fully-fledged array programming language.     

A feature-oriented approach for developing reusable product line assets of service-based systems

Service orientation (SO) is a relevant promising candidate for accommodating rapidly changing user needs and expectations. One of the goals of adopting SO is the improvement of reusability, however, the development of service-based system in practice has uncovered several challenging issues, such as how to identify reusable services, how to determine configurations of services that are relevant to users’ current product configuration and context, and how to maintain service validity after configuration changes. In this paper, we propose a method that addresses these issues by adapting a feature-oriented product line engineering approach. The method is notable in that it guides developers to identify reusable services at the right level of granularity and to map users’ context to relevant service configuration, and it also provides a means to check the validity of services at runtime in terms of invariants and pre/post-conditions of services. Moreover, we propose a heterogeneous style based architecture model for developing such systems.     

一种面向特征的软件产品线非功能需求建模方法

分析传统非功能需求定义的不足,基于需求分析阶段的系统抽象—"需求模型"重新定义非功能需求,规范并简化功能需求与非功能需求之间的关系。扩展面向特征的软件产品线建模方法,在特征模型中显式地建模功能需求、非功能需求、非功能需求类型以及它们之间的相互关系,沿用传统特征模型中固有的变化性建模机制建模并管理非功能需求的变化性,显式地复用与非功能需求相关的建模知识和资产,为进一步研究定量评估产品线变体质量的新技术奠定基础。设计了一个基于多视图的特征建模方法,指导开发者在迭代的过程中建模非功能需求和功能需求,支持关注点分离和模型的复杂性管控。实现了工具原型并进行了实例验证。     

Context Dependent Procedures and Computed Types in eriFun

We present two enhancements of the functional language which is used in the eriFun system to write programs and formulate statements about them. Context dependent procedures allow to stipulate the context under which procedures are sensibly executed, thus avoiding runtime tests in program code as well as verification of absence of exceptions by proving stuck-freeness of procedure calls. Computed types lead to more compact code, increase the readability of programs, and make the well-known benefits of type systems available to non-freely generated data types as well. Since satisfaction of context requirements as well as type checking becomes undecidable, proof obligations are synthesized to be proved by the verifier at hand, thus supporting static code analysis. Information about the type hierarchy is utilized for increasing the performance and efficiency of the verifier.     

Invariant based programming: basic approach and teaching experiences

Program verification is usually done by adding specifications and invariants to the program and then proving that the verification conditions are all true. This makes program verification an alternative to or a complement to testing. We describe here another approach to program construction, which we refer to as invariant based programming, where we start by formulating the specifications and the internal loop invariants for the program, before we write the program code itself. The correctness of the code is then easy to check at the same time as one is constructing it. In this approach, program verification becomes a complement to coding rather than to testing. The purpose is to produce programs and software that are correct by construction. We present a new kind of diagrams, nested invariant diagrams, where program specifications and invariants (rather than the control) provide the main organizing structure. Nesting of invariants provide an extension hierarchy that allows us to express the invariants in a very compact manner. We have studied the feasibility of formulating specifications and loop invariants before the code itself has been written in a number of case studies. Our experience is that a systematic use of figures, in combination with a rough idea of the intended behavior of the algorithm, makes it rather straightforward to formulate the invariants needed for the program, to construct the code around these invariants and to check that the resulting program is indeed correct. We describe our experiences from using invariant based programming in practice, both from teaching programmers how to construct programs that they prove correct themselves, and from teaching invariant based programming for CS students in class. D. A. Duce, J. Oliveira, P. Boca and R. Boute