The Correctness-by-Construction Approach to Programming
The Correctness-by-Construction Approach to Programming
复制标题
构造正确性编程方法
DOI：
10.1007/978-3-642-27919-5
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
B. Watson
中科院分区：
文献类型：
--
作者：
D. Kourie;B. Watson
这本书的重点是弥合两种极端的软件开发方法之间的差距。一方面，有些文本和方法是如此正式，以至于吓跑了除了最专注的理论计算机科学家之外的所有人。另一方面，也有一些人认为，任何形式的衡量都是浪费时间，导致软件是按照直觉开发的。Kourie和Watson倡导一种被称为构造正确性的方法，这是一种依赖于形式理论来推导算法的技术，但这需要以非常系统和务实的方式部署这种理论。首先，它们提供了理解和应用该方法所需的关键理论背景(如一阶谓词逻辑或求精定律)。然后，他们详细介绍了从二进制搜索到格子覆盖图构造和有限自动机最小化的一系列分级示例，以展示它如何应用于日益复杂的算法问题。这本书的主要目的是改变软件开发人员在小规模编程层面上处理任务的方式，以期提高代码质量。因此，它既符合IEEEs的软件工程知识体系指南(SWEBOK)建议，它确定了本书中所涵盖的主题，作为软件工程师工具和方法武器库的一部分，也符合软件工程方法和理论(Semat)计划的目标，该计划旨在基于坚实的理论重新发现软件工程。
The focus of this book is on bridging the gap between two extreme methods for developing software. On the one hand, there are texts and approaches that are so formal that they scare off all but the most dedicated theoretical computer scientists. On the other, there are some who believe that any measure of formality is a waste of time, resulting in software that is developed by following gut feelings and intuitions. Kourie and Watson advocate an approach known as correctness-by-construction, a technique to derive algorithms that relies on formal theory, but that requires such theory to be deployed in a very systematic and pragmatic way. First they provide the key theoretical background (like first-order predicate logic or refinement laws) that is needed to understand and apply the method. They then detail a series of graded examples ranging from binary search to lattice cover graph construction and finite automata minimization in order to show how it can be applied to increasingly complex algorithmic problems. The principal purpose of this book is to change the way software developers approach their task at programming-in-the-small level, with a view to improving code quality. Thus it coheres with both the IEEEs Guide to the Software Engineering Body of Knowledge (SWEBOK) recommendations, which identifies themes covered in this book as part of the software engineers arsenal of tools and methods, and with the goals of the Software Engineering Method and Theory (SEMAT) initiative, which aims to refound software engineering based on a solid theory.