Search

International audience; We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsistencies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hocmathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards

Relative correctness is the property of a program to be more-correct than another program with respect to a given specification. Among the many properties of relative correctness, that which we found most intriguing is the property that program P' refines program P if and only if P' is more-correct than P with respect to any specification. This inspires us to reconsider program derivation by successive refinements: each step of this process mandates that we transform a program P into a program P' that refines P, i.e. P' is more-correct than P with respect to any specification. This raises the question: why should we want to make P' more-correct than P with respect to any specification, when we only have to satisfy specification R? In this paper, we discuss a process of program derivation that replaces traditional sequence of refinement-based correctness-preserving transformations starting from specification R by a sequence of relative correctness-based correctness-enhancing transformations starting from abort., In Proceedings Refine'15, arXiv:1606.01344

Pattern matching is advantageous for understanding and reasoning about function definitions, but it tends to tightly couple the interface and implementation of a datatype. Significant effort has been invested in tackling this loss of modularity; however, decoupling patterns from concrete representations while maintaining soundness of reasoning has been a challenge. Inspired by the development of invertible programming, we propose an approach to abstract datatypes based on a rightinvertible language rinv-every function has a right (or pre-) inverse.We show how this new design is able to permit a smooth incremental transition from programs with algebraic datatypes and pattern matching, to ones with proper encapsulation (implemented as abstract datatypes), while maintaining simple and sound reasoning. © 2010 Springer-Verlag Berlin Heidelberg.

International audience; We validate the RBAC ANSI 2012 standard using the B method. Numerous problems are identified: logical errors, inconsisten- cies, ambiguities, typing errors, missing preconditions, invariant violation, inappropriate specification notation. A clean version of the standard written in the B notation is proposed. We argue that the ad hoc mathematical notation used in the standard is inappropriate and we propose that a more methodological and tool-supported approach must definitely be used for writing standards, in order to avoid the issues identified in the paper. Human reviewing is insufficient to produce error-free international standards

Traditional programming calculi focus on transforming a~specification into a~program. With the advent of such recent paradigms as white box reuse, component-based software development, and re-engineering, and with the continued predominance of software maintenance, less and less software engineering activity nowadays deals with straightforward development. More and more, software products are derived by incrementing, composing, merging, or otherwise modifying existing components. In this paper we present a~calculus that models these paradigms.

We give a formal relation-based definition of scenarios and we show how different scenarios can be integrated to obtain a more global view of user-system interactions. We restrict ourselves to the sequential case, meaning that we suppose that there is only one user (thus, the scenarios we wish to integrate cannot occur concurrently). Our view of scenarios is state-based, rather than event-based, like most of the other approaches, and can be grafted to the well-established specification language Z. Also, the end product of scenario integration, the specification of the functional aspects of the system, is given as a relation; this specification can be refined using independently developed methods. Our formal description is coupled with a diagram-based, transition-system like, presentation of scenarios, which is better suited to communication between clients and specifiers.

Given a specification that includes a number of user requirements, we wish to focus on the requirements in turn, and derive a partly defined program for each; then combine all the partly defined programs into a single program that satisfies all the requirements simultaneously. In this paper we introduce a mathematical basis for solving this problem, and we illustrate it by means of a simple example.

The design of modules in modular languages, and the model of software development activities portrayed by it, have been well received in batch environments. However, from their experience in the design of the MUPE-2 integrated programming environment, the authors hold the opinion that the model of software activities portrayed by modules in a batch environment is not entirely appropriate in an integrated programming environment. In adapting modules to the MUPE-2 environment, the authors have changed their design and implementation. In particular, they have added a module type, called the supermodule, that can encapsulate related modules, so that the architecture of a software system may be captured, and unified the separate definition and implementation parts of a module into a single module, called the DefImp module, so that some consistency problems due to textual separation can be avoided. They examine the role of modules in a batch environment and give a rationale for their design of modules for integrated environments. >

In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalize this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behavior of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is diffcult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalization of the while statement verification rule to nondeterministic loops.

Traditional programming paradigms revolve around mapping a single requirements specification into a program. As less and less software is developed from scratch, and more and more is developed from existing software artifacts, this traditional paradigm is growing less and less predominant. Paradigms that are gaining ground include: Program adaptation, whereby a program is modified to satisfy a specification that it does not originally satisfy; this occurs in adaptive software maintenance and in white box software reuse. Software Incrementation, whereby a program is modified to have an additional functional feature, while preserving its current functional properties. Software Merging, whereby two (typically) similar software products are merged into a single product that cumulates the functional features of each; this arises typically when the two products are obtained by software incrementation from a common base version. Software Composition, whereby various existing reusable assets are composed together (by means of application-specific code) to produce a prespecified software application; this arises in component-based software development.

In Chapter 8, it was shown how functional programs can be regarded as elements of a relation algebra. In this chapter, we consider imperative programs, which we view as computing an input-output relation on a set of states. We are interested here in programs that are meant to terminate, not in reactive programs. Our programming language is Dijkstra’s language of guarded commands [Dijkstra 1976], which allows the expression of nondeterminism, thus making a relational approach very natural.

Given a specification that includes a number of user requirements, we wish to focus on the requirements in turn, and derive a partly defined program for each; then combine all the partly defined programs into a single program that satisfies all the requirements simultaneously. In this paper we introduces a mathematical basis for solving this problem; and we illustrate it by means of a simple example.

Of the many ways to express program specifications, three of the most common are: as a pair of assertions, an input assertion and an output assertion; as a function mapping legal inputs to correct outputs; or as a relation containing the input/output pairs that are considered correct. The construction of programs consists of mapping a potentially complex specification into a program by recursively decomposing complex specifications into simpler ones. We show how this decomposition takes place in all three modes of specification and draw some conclusions on the nature of programming.

Given a software library whose entries are represented by formal specifications, we distinguish between two retrieval procedures: exact retrieval, whereby, given a query K, we identify all the library components that are correct with respect to K; approximate retrieval, which is invoked when exact retrieval fails, and identifies the library components that minimize adaptation effort. To this effect, we define four measures of functional distance between specifications, and discuss algorithms that minimize these measures over a set of components; then we discuss whether these measures can be used to predict adaptation effort.