Article

Free access

Formal specification as a design tool

Authors:

John Guttag,

J. J. HorningAuthors Info & Claims

POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 251 - 261

https://doi.org/10.1145/567446.567471

Published: 28 January 1980 Publication History

PDF eReader

Abstract

The formulation and analysis of a design specification is almost always of more utility than the verification of the consistency of a program with its specification. Good specification tools can assist in this process, but have generally not been proposed and evaluated in this light. In this paper we outline a specification language combining algebraic axioms and predicate transformers, present part of a non-trivial example (the specification of a high-level interface to a display), and finally discuss the analysis of this specification.

References

[1]

{Dijkstra 76} E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.

Digital Library

Google Scholar

[2]

{Goguen 78} J. A. Goguen, J. W. Thatcher, and E. G. Wagner, "An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types," Current Trends in Programming Methodology Volume IV (ed. Raymond T. Yeh), Prentice-Hall, 1978.

Google Scholar

[3]

{Guttag 77} J. V. Guttag, "Abstract Data Types and the Development of Data Structures," Comm. ACM20, 6, pp. 396-404, June 1977.

Digital Library

Google Scholar

[4]

{Guttag 78} J. V. Guttag and J. J. Horning, "The Algebraic Specification of Abstract Data Types," Acta Informatica10, 1, pp. 27-52, 1978.

Google Scholar

[5]

{Guttag 79} J. V. Guttag, "Notes on Type Abstraction," Proc. Specifications of Reliable Software Conference, IEEE Cat. No. 79 CHI401-9C, pp. 36-46, April 1979.

Google Scholar

[6]

{Liskov 77} B. H. Liskov and S. N. Zilles, "An Introduction to Formal Specifications of Data Abstractions," Current Trends in Programming Methodology, Volume I, (ed. Raymond Yeh), Prentice-Hall, 1977.

Google Scholar

Cited By

View all

Vijayalayan KHarwood AKarunasekera S(2013)Distributed scheduling schemes for wireless mesh networksACM Computing Surveys10.1145/2522968.252298246:1(1-34)Online publication date: 11-Jul-2013
https://dl.acm.org/doi/10.1145/2522968.2522982
Tamburri DLago PVliet H(2013)Organizational social structures for software engineeringACM Computing Surveys10.1145/2522968.252297146:1(1-35)Online publication date: 11-Jul-2013
https://dl.acm.org/doi/10.1145/2522968.2522971
Arenas MPérez JReutter J(2013)Data exchange beyond complete dataJournal of the ACM10.1145/2508028.250598560:4(1-59)Online publication date: 4-Sep-2013
https://dl.acm.org/doi/10.1145/2508028.2505985
Show More Cited By

Recommendations

Design and Implementation of a Tool for Specifying Specification in SOFL
Revised Selected Papers of the Second International Workshop on Structured Object-Oriented Formal Language and Method - Volume 7787

Structure Object-oriented Formal Language SOFL is not just a formal language for writing formal specification. It is also an approach and a methodology. SOFL provides a three-step approach for modelling a software system using formal specification. ...
Formal Specification of User Interfaces: A Comparison and Evaluation of Four Axiomatic Approaches
Annals of discrete mathematics, 24

Few examples of formal specification of the semantics of user interfaces exist in the literature. This paper presents a comparison of four axiomatic approaches which we have applied to the specification of a commercial user interface-the line editor for ...
Formal Specification and Design Time Testing

It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1980

261 pages

ISBN:0897910117

DOI:10.1145/567446

Conference Chairs:
Paul Abrahams
Courant Institute, New York, NY
,
Richard Lipton
University of California at Berkeley, Berkeley, CA
,
Program Chair:
Stephen Bourne
Bell Laboratories, Murray Hill, NJ

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 January 1980

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

78
Total Citations
View Citations
750
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)13

Reflects downloads up to 08 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Vijayalayan KHarwood AKarunasekera S(2013)Distributed scheduling schemes for wireless mesh networksACM Computing Surveys10.1145/2522968.252298246:1(1-34)Online publication date: 11-Jul-2013
https://dl.acm.org/doi/10.1145/2522968.2522982
Tamburri DLago PVliet H(2013)Organizational social structures for software engineeringACM Computing Surveys10.1145/2522968.252297146:1(1-35)Online publication date: 11-Jul-2013
https://dl.acm.org/doi/10.1145/2522968.2522971
Arenas MPérez JReutter J(2013)Data exchange beyond complete dataJournal of the ACM10.1145/2508028.250598560:4(1-59)Online publication date: 4-Sep-2013
https://dl.acm.org/doi/10.1145/2508028.2505985
Wang HZhou G(2012)Toward a Unified Framework for Standard and Update Multi-Document SummarizationACM Transactions on Asian Language Information Processing10.1145/2184436.218443811:2(1-18)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2184436.2184438
He Y(2012)Incorporating Sentiment Prior Knowledge for Weakly Supervised Sentiment AnalysisACM Transactions on Asian Language Information Processing10.1145/2184436.218443711:2(1-19)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2184436.2184437
Koo BSimmons WCrawley E(2007)A Valuation Technology for Product Development Options Using an Executable Meta-modeling LanguageComplex Systems Concurrent Engineering10.1007/978-1-84628-976-7_13(107-115)Online publication date: 2007
https://doi.org/10.1007/978-1-84628-976-7_13
Bailey BAdamczyk PChang TChilson N(2006)A framework for specifying and monitoring user tasksComputers in Human Behavior10.1016/j.chb.2005.12.01122:4(709-732)Online publication date: Jul-2006
https://doi.org/10.1016/j.chb.2005.12.011
Jackson D(2005)Abstract model checking of infinite specificationsFME '94: Industrial Benefit of Formal Methods10.1007/3-540-58555-9_113(519-531)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-58555-9_113
Garlan D(2005)Formal methods for software engineers: Tradeoffs in curriculum designSoftware Engineering Education10.1007/3-540-55963-9_45(131-142)Online publication date: 11-Jul-2005
https://doi.org/10.1007/3-540-55963-9_45
Sannella DTarlecki A(2005)Toward formal development of programs from algebraic specifications: Model-theoretic foundationsAutomata, Languages and Programming10.1007/3-540-55719-9_112(656-671)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-55719-9_112
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Design and Implementation of a Tool for Specifying Specification in SOFL

Formal Specification of User Interfaces: A Comparison and Evaluation of Four Axiomatic Approaches

Formal Specification and Design Time Testing