Title :
A Specification Method for Specifying Data and Procedural Abstractions
Author :
Claybrook, Billy G.
Author_Institution :
MITRE Corporation
Abstract :
A specifilcation method designed primarily for specifying data abstractions, but suitable for specifying procedural abstractions as well, is described. The specification method is based on the abstract model approach to specifying abstractions. Several data abstractions and procedural abstractions are specified and a proof of implementation correctness is given for one of the data abstractions–a symbol table.
Keywords :
Data abstraction; formal specification; implementation correctness; procedural abstraction; Databases; Design methodology; Formal specifications; Helium; Problem-solving; Programming profession; Data abstraction; formal specification; implementation correctness; procedural abstraction;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1982.235735