article

Free access

More thoughts on specification and verification

Author:

J. A. GoguenAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 6, Issue 3

Pages 38 - 41

https://doi.org/10.1145/1010832.1010845

Published: 01 July 1981 Publication History

PDF eReader

References

[1]

{Abriel, Schuman & Meyer 79} Abrial, J. R., Schuman, S. A., and Meyer, B. Specification Language (draft). 1979. Cambridge University.

Google Scholar

[2]

{Boyer & Moore 80} Boyer, R. and Moore, J. S. A Computational Logic. Academic Press, 1980.

Google Scholar

[3]

{Burstall & Darlington 77} Burstall, R. M. and Darlington, J. A Transformation System for Developing Recursive Programs. JACM 24(1):44--67, 1977.

Digital Library

Google Scholar

[4]

{Burstall & Goguen 77} Burstall, R. M. and Goguen, J. A. Putting Theories together to Make Specifications. Proc. 5th Int. Joint Confr. on Artificial Intelligence, 1977.

Google Scholar

[5]

{Burstall & Goguen 80} Burstall, R. M., and Goguen, J. A. The Semantics of CLEAR, a Specification Language. In Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, Lecture Notes in Computer Science, volume 86, pages 292--332. Springer-Verlag, 1980.

Digital Library

Google Scholar

[6]

{Burstall, MacQueen and Sanella 80} Burstall, R. M., MacQueen, D. and Sanella, D. HOPE: an Experimental Applicative Language. In Conference Record of the 1980 LISP Conference. Stanford University, 1980. pages 136--143.

Digital Library

Google Scholar

[7]

{Gerhard, Musser et al 79} Gerhard, S. L., Musser, D. R., Thompson, D. H., Baker, D. A., Bates, R. W., Erickson, R. W., London, R. L., Taylor, D. G., and Wile, D. S. An Overview of AFFIRM: A Specification and Verification System. Technical Report, USC Information Sciences Institute, Marina del Rey, CA, 1979.

Google Scholar

[8]

{Goguen & Burstall 80a} Goguen, J. A. and Burstall, R. M. An Ordinary Design. Technical Report, SRI International, 1980. Draft report.

Google Scholar

[9]

{Goguen & Burstall 80b} Goguen, J. A., and Burstall, R. M. CAT, a System for the Structured Elaboration of Correct Programs from Structured Specifications. Technical Report, SRI, International; Computer Science Lab, 1980. Based on unpublished working draft, UCLA and SRI, 1979.

Google Scholar

[10]

{Goguen & Tardo 79} Goguen, J. A. and Tardo, J. An Introduction to OBJ-T. In Specification of Reliable Software, pages 170--189. IEEE, 1979. Cambridge, Mass., April 1979.

Google Scholar

[11]

{Goguen 80} Goguen, J. A. Thoughts on Program Specification, Design and Verification. Software Engineering Notes 5(3), 1980. Association for Computing Machinery, Special Interest Group on Software Engineering.

Google Scholar

[12]

{Guttag, Horowitz & Musser 78} Guttag, J. V., Horowitz, E. and Musser, D. R. Abstract Data Types and Software Validation. Communications of the ACM, 1978.

Digital Library

Google Scholar

[13]

{Guttag 75} Guttag, J. V. The Specification and Application to Programming of Abstract Data Types. PhD thesis, Univ. of Toronto, 1975.

Digital Library

Google Scholar

[14]

{Levitt, Robinson & Silverberg 79} Levitt, K., Robinson, L. and Silverberg, B. The HDM Handbook, vols. I, II, III. Technical Report, SRI, International; Computer Science Lab, 1979.

Google Scholar

[15]

{Moriconi & Schwartz 81} Moniconi, M. and Schwartz, R. L. Automatic Construction of Verification Condition Generators from Hoare Logics. In Proceedings, 8th International Colloquium on Automata, Languages, and Programming. Springer-Verlag, Lecture Notes in Computer Science, 1981. Haifa, Israel.

Digital Library

Google Scholar

[16]

{Neumann, Boyer, Feiertag, Levitt & Robinson 77} Neumann, P. G., Boyer, R. S., Feiertag, R. S., Levitt, K. N. and Robinson, R. S. A Provably Secure Operating System: The System, its Applications, and Proofs. Technical Report, SRI International, Computer Science Laboratory, 1977.

Google Scholar

Cited By

View all

Sorensen D(2024)(In)Correct Smart Contract Specifications2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)10.1109/ICBC59979.2024.10634444(567-575)Online publication date: 27-May-2024
https://doi.org/10.1109/ICBC59979.2024.10634444
Alexandre FBsaïes K(1997)A Methodology For Constructing Logic ProgramsFundamenta Informaticae10.5555/2379336.237933729:3(203-223)Online publication date: 1-Aug-1997
https://dl.acm.org/doi/10.5555/2379336.2379337
Graves HPolak W(1992)Common intermediate design languageProceedings of the Twenty-Fifth Hawaii International Conference on System Sciences10.1109/HICSS.1992.183264(497-506 vol.2)Online publication date: 1992
https://doi.org/10.1109/HICSS.1992.183264
Show More Cited By

More thoughts on specification and verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of ...
Specification and automated verification of concurrent software systems
Experiences with specification and verification in LOTOS: a report on two case studies
WIFT '95: Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques

We consider the problems of verifying properties of LOTOS specifications with specific reference to two case studies, one of which was proposed by an industrial collaborator. The case studies present quite different verification requirements and we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 6, Issue 3

July 1981

104 pages

ISSN:0163-5948

DOI:10.1145/1010832

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1981

Published in SIGSOFT Volume 6, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
279
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)4

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Sorensen D(2024)(In)Correct Smart Contract Specifications2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)10.1109/ICBC59979.2024.10634444(567-575)Online publication date: 27-May-2024
https://doi.org/10.1109/ICBC59979.2024.10634444
Alexandre FBsaïes K(1997)A Methodology For Constructing Logic ProgramsFundamenta Informaticae10.5555/2379336.237933729:3(203-223)Online publication date: 1-Aug-1997
https://dl.acm.org/doi/10.5555/2379336.2379337
Graves HPolak W(1992)Common intermediate design languageProceedings of the Twenty-Fifth Hawaii International Conference on System Sciences10.1109/HICSS.1992.183264(497-506 vol.2)Online publication date: 1992
https://doi.org/10.1109/HICSS.1992.183264
Graves HSelfridge P(1991)Lockheed environment for automatic programmingProceedings of the 6th International Conference on Knowledge-Based Software Engineering10.1109/KBSE.1991.638022(68-76)Online publication date: 22-Sep-1991
https://dl.acm.org/doi/10.1109/KBSE.1991.638022
Collberg CKrampell M(1987)A property-based method for selecting among multiple implementations of modulesESEC '8710.1007/BFb0022112(191-201)Online publication date: 1987
https://doi.org/10.1007/BFb0022112
Naur P(1982)Formalization in program developmentBIT10.1007/BF0193440822:4(437-453)Online publication date: Dec-1982
https://doi.org/10.1007/BF01934408
Levitt KNeumann P(1981)Recent SRI work in verificationACM SIGSOFT Software Engineering Notes10.1145/1010832.10108436:3(27-35)Online publication date: 1-Jul-1981
https://dl.acm.org/doi/10.1145/1010832.1010843

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.

References

Cited By

Recommendations

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

Specification and automated verification of concurrent software systems

Experiences with specification and verification in LOTOS: a report on two case studies

Comments

Information

Published In

Publisher

Publication History

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations