Theories of Programming - The Life and Works of Tony Hoare
Theories of Programming - The Life and Works of Tony Hoare
复制标题
编程理论 - 托尼·霍尔的生平和著作
DOI：
10.1145/3477355.3477365
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Brookes S
中科院分区：
文献类型：
--
作者：
Brookes S
在本章中，我们将介绍CSP是如何开发的：语言、语义、实现和机械化验证工具。我们展示了如何细化检查FDR的演变，我们调查了一些实际应用的例子，这些发展的启发。其中包括形式方法的一些最令人兴奋的工业和学术应用。总的来说，我们想证明CSP框架以自然的方式将理论与实践相结合，并广泛适用于真实的世界。这种结合，由直觉，理论研究和工具开发之间的相互作用驱动，是托尼对科学和研究的典型态度。CSP和FDR的故事的第一部分相当于重新讲述了比尔在1994年在牛津举行的托尼60岁生日庆典上所讲述的历史[Roscoe 1994]，在这里提供了事后诸葛亮的好处。Steve补充说
In this chapter, we look at how CSP was developed: the language, its semantics, its implementation, and mechanized verification tools. We show how the refine ment checker FDR evolved, and we survey some examples of practical applications inspired by these developments. These include some of the most exciting industrial and academic applications of formal methods. Overall, we want to demonstrate that the CSP framework combines theory with practice in a natural manner and is widely applicable in the real world. This kind of combination, driven by an inter play between intuition, theoretical investigation, and tool development, is typical of Tony’s attitude towards science and research. The first part of the story of CSP and FDR amounts to a re-telling of the history recounted in Bill’s contribution to Tony’s 60th birthday Festschrift, held at Oxford in 1994 [Roscoe 1994], offered here with the benefit of hindsight. Steve has added