Abstract: The aim of this paper is to merge two approaches of software development. The first one is the component approach. Developping software components is now a technique widely used by the software industry. The second approach is the formal one. These approaches are not so distant if we consider Bertrand Meyer’s opinion: a component without contracts can not be reused (more exactly, he said that it was more complicated to reuse such a component). One of the difficulties with the design by contract approach is to find the contracts. In some formal approach -we will use the B method in this paper- the software properties (the contracts) are expressed in the specifications. We present in this paper an approach to generate code in the spirit of the component approach from B specifications.
Abstract: The aim of this paper is to merge two approaches of software development. The first one is the component approach. Developping software components is now a technique widely used by the software industry. The second approach is the formal one. These approaches are not so distant if we consider Bertrand Meyer’s opinion: a component without contracts can not be reused (more exactly, he said that it was more complicated to reuse such a component). One of the difficulties with the design by contract approach is to find the contracts. In some formal approach -we will use the B method in this paper- the software properties (the contracts) are expressed in the specifications. We present in this paper an approach to generate code in the spirit of the component approach from B specifications.
Notes: Special topic session of the Seventh Conference on Integrated Design and Process Technology. Selected paper for SDPS. ISSN 1090-9389
Abstract: In this paper, we present a new approach to generating different codes from specifications developped with the B method. This code generator is based on the flattening algorithm and the use of a rewriting tool (an XSLT processor, for example). Currently, the commercial code generation processors are black box tools, and it is very difficult to modify them. We will show that our approach simplifies code generation specification, which makes the specification of new code generators for new target languages easier and faster. Another benefit of our approach is that it allows assertions to be added to the code generated. Assertions, are expressed in the specifications but they are forgot in the current code generation process.
Abstract: The aim of this paper is to merge two approaches of software development. The first one is the component approach. Developping software components is now a new challenge in the software industry. The second approach is the formal one. These approaches are not so distant if we consider B. Meyer’s opinion: a component without contracts can not be reused (more rigorously, he said that it was more complicated to reuse such a component). One of the difficulties with the design by contract approach is to find the contracts. In some formal approach -we will use the $B$ method in this paper- the software properties (the contracts) are expressed in the specifications. We present in this paper a tool we have developped to generate code from $B$ specifications. We will see how we can link the notion of component and the $B$ specifications.
