Abstract data types and software validation
作者： John V. Guttag , Ellis Horowitz , David R. Musser
关键词: Computer science 、 Data type 、 Algebraic number 、 Specification language 、 Data structure 、 Correctness 、 Theoretical computer science 、 Mathematical proof 、 Abstract data type 、 Axiom 、 Programming language 、 Formal specification 、 General Computer Science
摘要: A data abstraction can be naturally specified using algebraic axioms. The virtue of these axioms is that they permit a representation-independent formal specification type. An example given which shows how to employ at successive levels implementation. major thrust the paper twofold. First, it shown use axiomatizations simplify process proving correctness an implementation abstract Second, semi-automatic tools are described used both automate such proofs and derive immediate from This allows for limited testing programs design time, before conventional accomplished.
acm.org
ucsb.edu 
sci-hub.se 参考文章(20)
Ole-Johan Dahl, SIMULA 67 common base language, (Norwegian Computing Center. Publication) ,(1968)
Norihisa Suzuki, Automatic verification of programs with complex data structure ,(1976)
David Lorge. Parnas, Information distribution aspects of design methodology ifip congress. pp. 339- 344 ,(2012) , 10.1184/R1/6606470.V1
Zohar Manna, Mathematical Theory of Computation Dover Publications, Incorporated. ,(2003)
Ben Wegbreit, Jay M. Spitzen, Proving Properties of Complex Data Structures Journal of the ACM. ,vol. 23, pp. 389- 396 ,(1976) , 10.1145/321941.321957
Robert S. Boyer, J. Strother Moore, Proving Theorems about LISP Functions Journal of the ACM. ,vol. 22, pp. 129- 144 ,(1975) , 10.1145/321864.321875
John V. Guttag, David R. Musser, Ellis Horowitz, The design of data type specifications international conference on software engineering. pp. 414- 420 ,(1976) , 10.5555/800253.807714
W.A. Wulf, R.L. London, M. Shaw, An Introduction to the Construction and Verification of Alphard Programs IEEE Transactions on Software Engineering. ,vol. SE-2, pp. 253- 265 ,(1976) , 10.1109/TSE.1976.233830
R. D. Jenks, The SCRATCHPAD language Sigplan Notices. ,vol. 9, pp. 101- 111 ,(1974) , 10.1145/800233.807051
C. A. R. Hoare, Recursive data structures International Journal of Parallel Programming. ,vol. 4, pp. 105- 132 ,(1975) , 10.1007/BF00976239