Reducing problem-solving variance to improve predictability
Reducing problem-solving variance to improve predictability
复制标题
减少解决问题的方差以提高可预测性
DOI：
10.1145/108515.108531
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
J. Strosnider
中科院分区：
文献类型：
--
作者：
C. J. Paul;A. Acharya;B. Black;J. Strosnider
证明作为助理。在这种情况下，正式开发是通过一系列经过正式证明的步骤，从正式规范中推导出一个实现。正如我们所熟知的，只有有一个工具来检查形式链是否被打破，并提供一些指导，这才是实用的。作者考虑了VDM的开发和每个开发步骤的相应证明义务，主要是数据验证和操作分解。案例研究是一个机器人控制器，使用的工具是B定理证明器。V - D - M开发被表示为一组B规则；然后，该工具能够自动生成证明义务（并自动证明其中的一些义务）。•在这个案例研究中特别有趣的是，vdd开发的B中的形式化是独立于案例研究的，并且可以在其他问题中重用。另一个有趣的副产品是重用经过验证的正式开发的部分的可能性。事实证明，只有B是不够的，更多的VDM开发方面的专业知识可以在开发中提供更多的指导。然而，作者证明了支持正式的开发现在是可行的，即使它还不像将来广泛使用那样容易。•Wileden、Wolf、Rosenblatt和Tarr针对软件开发和重用中一个古老但重要的问题提出了一个解决方案：用不同语言开发和/或运行在不同机器上的组件的互操作性。他们的文章介绍了用于实现异构软件组件通信的各种现有方法。然后，作者提出了基于抽象数据类型概念的自己的方法。这看起来很自然，因为信息隐藏的概念与此相关。因此，所建议的方法提供了一种在规范级别上允许互操作性的方法。提供了用于描述抽象数据类型和此类类型的语言绑定的符号。描述了一个原型，它允许类型定义、语言绑定，并提供了一个最常见的数据类型库。很明显，这种方法将对下一代开发环境产生极大的兴趣，因为许多不同类型的对象（通过不同的语言进行操作）必须以一种方便和透明的方式进行管理。•Prieto-Dfaz报告的经验讨论了对……
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 hiding is relevant here. Thus, the proposed method provides a way to allow interoperability at the specification level. A notation for describing abstract data types and language bindings of such types is provided. A prototype is described which allows type definition, language bindings, and provides a library of most common datatypes. It is clear that this approach will be of high interest for the next generation of development environments since many different types of objects, manipulated via different languages, must be managed in a convenient and transparent way. • The experience reported by Prieto-Dfaz discusses the implementation of a classification scheme for …