Safe Data Type Specifications

1 May 1984

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering

Vol. SE-10 (3) , 285-289
https://doi.org/10.1109/tse.1984.5010237

Abstract

This paper discusses the current style of algebraic data type specifications. Some simple examples illustrate that whether or not two objects of the type being specified are equal can be implementation dependent, even for very simple objects of the type. To remedy this, it is proposed that specifications should be safe, where safety is a stronger requirement than Guttag's sufficient completeness. The paper also discusses when an operator should be part of a specification and when it should be introduced by extension, and concludes with safe specifications of some common data types.

Keywords

This publication has 7 references indexed in Scilit:

Data Abstraction, Implementation, Specification, and Testing
ACM Transactions on Programming Languages and Systems, 1981
Notes on Type Abstraction (Version 2)
IEEE Transactions on Software Engineering, 1980
Abstract Data Type Specification in the Affirm System
IEEE Transactions on Software Engineering, 1980
Abstract data types and software validation
Communications of the ACM, 1978
The algebraic specification of abstract data types
Acta Informatica, 1978
An Introduction to the Construction and Verification of Alphard Programs
IEEE Transactions on Software Engineering, 1976
Proof of correctness of data representations
Acta Informatica, 1972