Algebraic specification of data types: A synthetic approach
Algebraic specification of data types: A synthetic approach
复制标题
数据类型的代数规范：一种综合方法
DOI：
10.1007/bf01752392
复制
发表时间：
1981
期刊：
影响因子：
--
通讯作者：
M. Smyth
中科院分区：
文献类型：
--
作者：
D. Lehmann;M. Smyth
对数据类型的概念进行了数学解释，它允许过程数据类型和循环定义的数据类型。这种解释似乎为大多数计算机科学家所说的数据类型、数据结构、类型、模式、集群或类提供了一个很好的模型。本文的精神是麦卡锡[43]和霍尔[18]的精神。数学处理是将Scott关于区域方程[34]、[35]和[36]的解的思想与adj群(adj[2]和[3])注意到的初始性相结合。本工作在Scott提出的数据类型的基础上增加了运算，并提出了一种替代Guttag[14]、Guttag和Horning[15]和adj[2]等式规范的方法。这种数学解释的优点如下：揭示了高级编程语言中一些难以理解的结构，简化了编写正确程序的任务，并为程序或实现提供了可能的正确性证明。
A mathematical interpretation is given to the notion of a data type, which allows procedural data types and circularly defined data types. This interpretation seems to provide a good model for what most computer scientists would call data types, data structures, types, modes, clusters or classes. The spirit of this paper is that of McCarthy [43] and Hoare [18]. The mathematical treatment is the conjunction of the ideas of Scott on the solution of domain equations [34], [35], and [36] and the initiality property noticed by the ADJ group (ADJ [2] and [3]). The present work adds operations to the data types proposed by Scott and proposes an alternative to the equational specifications proposed by Guttag [14], Guttag and Horning [15] and ADJ [2]. The advantages of such a mathematical interpretation are the following: throwing light on some ill-understood constructs in high-level programming languages, easing the task of writing correct programs and making possible proofs of correctness for programs or implementations.