Reducing problem-solving variance to improve predictability

摘要

bens offer a very convincing demonstration of a formal development in their article using a theorem prover as an assistant. A formal development, in this case, is the derivation of an implementation from a formal specification through a n u m b e r of formally proven steps. It is only practical, as we well know, if there is a tool to check that the formal chain is not broken and to provide some guidance. The authors consider VDM developments and the corresponding proof obligations for each development step, mainly data'verification and operation decomposition. The case study is a robot controller and the tool used is the B theorem prover. The V D M development was expressed as a set of B rules; the tool was then able to automatically generate the proof obligations (and to prove some of them automatically). What is especially interesting in this case study is that the formalization in B of the V D M development is independent of the case study and can be reused for other problems. Another interesting by-product is the possibility of reusing parts of proven formal developments. It turned out that B alone is not sufficient and that more expertise on VDM development would allow more guidance in the development. However, the authors demonstrate that supporting formal development is now feasible, even if it is not yet as easy as it must be some day for widespread use. Wileden, Wolf, Rosenblatt and Tarr propose a solution for an old, yet important, problem in software development and reuse: the interoperability of components developed in different languages and/or running on different machines. Their article presents a guided tour of various existing approaches for making heterogeneous software components communicate. The authors then present their own approach, which is based on the notion of abstract data types. It looks quite natural since the notion of information