{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T21:47:55Z","timestamp":1759960075987},"publisher-location":"Berlin, Heidelberg","reference-count":60,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_8","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1087-1106","source":"Crossref","is-referenced-by-count":24,"title":["Enhancing the pre- and postcondition technique for more expressive specifications"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert L.","family":"Baker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"8_CR1","series-title":"FACIT","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0987-7","volume-title":"A Theory and Practice of Program Development","author":"D. Andrews","year":"1997","unstructured":"Derek Andrews. A Theory and Practice of Program Development. FACIT. Springer-Verlag, London, UK, 1997."},{"issue":"6","key":"8_CR2","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R. J. R. Back","year":"1988","unstructured":"R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593\u2013624, August 1988.","journal-title":"Acta Informatica"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1016\/0304-3975(92)90309-4","volume":"100","author":"R. J. R. Back","year":"1992","unstructured":"R. J. R. Back and J. von Wright. Combining angels, deamons and miracles in program specifications. Theoretical Computer Science, 100(2):365\u2013383, June 1992.","journal-title":"Theoretical Computer Science"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"8_CR5","unstructured":"Alex Borgida, John Mylopoulos, and Raymond Reiter. \u2019... and nothing else changes\u2018: The frame problem in procedure specification. In Proceedings Fifteenth International Conference on Software Engineering, Baltimore, May 1993. Preliminary version obtained from the authors."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Martin B\u00fcchi and Emil Sekerinski. Formal methods for component software: The refinement calculus perspective. In Proceedings of the Second Workshop on Component-Oriented Programming (WCOP), June 1997. ftp:\/\/ftp.abo.fi\/pub\/cs\/papers\/mbuechi\/FMforCS.ps.gz .","DOI":"10.1007\/3-540-69687-3_68"},{"key":"8_CR7","unstructured":"Patrice Chalin. On the Language Design and Semantic Foundation of LCL, a Larch\/C Interface Specification Language. PhD thesis, Concordia University, 1455 de Maisonneuve Blvd. West, Montreal, Quebec, Canada, October 1995. Available as CU\/DCS TR 95-12, from the URL ftp:\/\/ftp.cs.concordia.ca\/pub\/chalin\/tr.ps.Z ."},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-60973-3_98","volume-title":"FME\u2019 96: Industrial Benefit and Advances in Formal Methods","author":"P. Chalin","year":"1996","unstructured":"Patrice Chalin, Peter Grogono, and T. Radhakrishnan. Identification of and solutions to shortcomings of LCL, a Larch\/C interface specification language. In Marie-Claude Gaudel and James Woodcock, editors, FME\u2019 96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 385\u2013404, New York, N.Y., March 1996. Springer-Verlag."},{"key":"8_CR9","unstructured":"David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto, Dec 1998."},{"key":"8_CR10","series-title":"Technical Report TR97-09","volume-title":"Behavioral subtyping in object-oriented languages","author":"K. K. Dhara","year":"1997","unstructured":"Krishna Kishore Dhara. Behavioral subtyping in object-oriented languages. Technical Report TR97-09, Department of Computer Science, Iowa State University, 226 Atanasoff Hall, Ames IA 50011-1040, May 1997. The author\u2019s Ph.D. dissertation."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258\u2013267. IEEE Computer Society Press, March 1996. A corrected version is Iowa State University, Dept. of Computer Science TR #95-20c.","DOI":"10.1109\/ICSE.1996.493421"},{"key":"8_CR12","unstructured":"E. W. Dijkstra, editor. Formal Development of Programs and Proofs. University of Texas at Austin Year of Programming series. Addison-Wesley Publishing Co., 1990."},{"key":"8_CR13","unstructured":"Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs, N.J., 1976."},{"key":"8_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and program semantics","author":"E. W. Dijkstra","year":"1990","unstructured":"Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and program semantics. Springer-Verlag, NY, 1990."},{"key":"8_CR15","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569777","volume-title":"Formal Specification and Design","author":"L. M. G. Feijs","year":"1992","unstructured":"L. M. G. Feijs and H. B. M. Jonkers. Formal Specification and Design, volume 35 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, 1992."},{"key":"8_CR16","unstructured":"John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools in Software Development. Cambridge, Cambridge, UK, 1998."},{"issue":"6","key":"8_CR17","doi-asserted-by":"publisher","first-page":"1044","DOI":"10.1109\/32.58789","volume":"16","author":"S. J. Garland","year":"1990","unstructured":"Stephen J. Garland, John V. Guttag, and James J. Horning. Debugging Larch Shared Language specifications. IEEE Transactions on Software Engineering, 16(6):1044\u20131057, September 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"8_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/BFb0015463","volume-title":"KORSO: Methods, Languages and Tools for the Construction of Correct Software","author":"M. Gogolla","year":"1995","unstructured":"M. Gogolla, S. Conrad, G. Denker, R. Herzig, N. Vlachantonis, and H. Ehrig. the language and its development environment. In Manfred Broy and Stefan J\u00e4hnichen, editors, KORSO: Methods, Languages and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science, pages 205\u2013220. Springer-Verlag, New York, N.Y., 1995."},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/102868.102870","volume":"34","author":"D. Gries","year":"1991","unstructured":"David Gries. Teaching calculation and discrimination: A more effective curriculum. Communications of the ACM, 34(3):44\u201355, March 1991.","journal-title":"Communications of the ACM"},{"key":"8_CR20","volume-title":"Texts and Monographs in Computer Science","author":"D. Gries","year":"1994","unstructured":"David Gries and Fred B. Schneider. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag, New York, N.Y., 1994."},{"key":"8_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/BFb0015254","volume-title":"Computer Science Today: Recent Trends and Developments","author":"D. Gries","year":"1995","unstructured":"David Gries and Fred B. Schneider. Avoiding the undefined by underspecification. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science, pages 366\u2013373. Springer-Verlag, New York, N.Y., 1995."},{"key":"8_CR22","unstructured":"M. Gurski and A. L. Baker. Testing SPECS-C++: A first step in validating distributed systems. In Intellegent Information Management Systems, pages 105\u2013108, Anaheim, 1994. The International Society for Mini and Microcomputers-ISMM."},{"key":"8_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"J. V. Guttag","year":"1993","unstructured":"John V. Guttag, James J. Horning, S.J. Garland, K.D. Jones, A. Modet, and J.M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, N.Y., 1993."},{"key":"8_CR24","unstructured":"I. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993."},{"key":"8_CR25","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569784","volume-title":"Programs, Recursion, and Unbounded Choice","author":"W. H. Hesselink","year":"1992","unstructured":"Wim H. Hesselink. Programs, Recursion, and Unbounded Choice, volume 27 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, N.Y., 1992."},{"issue":"10","key":"8_CR26","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576\u2013583, October 1969.","journal-title":"Communications of the ACM"},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(95)00042-B","volume":"54","author":"C.B. Jones","year":"1995","unstructured":"C.B. Jones. Partial functions and logics: A warning. Information Processing Letters, 54(2):65\u201367, 1995.","journal-title":"Information Processing Letters"},{"key":"8_CR28","volume-title":"International Series in Computer Science","author":"C. B. Jones","year":"1990","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.","edition":"second edition"},{"key":"8_CR29","unstructured":"Kevin D. Jones. LM3: A Larch interface language for Modula-3: A definition and introduction: Version 1.0. Technical Report 72, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301, June 1991. Order from src-report@src.dec.com."},{"key":"8_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-54834-3_26","volume-title":"VDM\u2019 91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, Volume 1: Conference Contributions","author":"H. B. M. Jonkers","year":"1991","unstructured":"H. B. M. Jonkers. Upgrading the pre-and postcondition technique. In S. Prehn and W. J. Toetenel, editors, VDM\u2019 91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, Volume 1: Conference Contributions, volume 551 of Lecture Notes in Computer Science, pages 428\u2013456. Springer-Verlag, New York, N.Y., October 1991."},{"key":"8_CR31","volume-title":"Formal Appoaches to Computing and Information Technology","author":"K. Lano","year":"1996","unstructured":"Kevin Lano. The B Language and Method: A guide to Practical Formal Development. Formal Appoaches to Computing and Information Technology. Springer-Verlag, London, UK, 1996."},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-0-585-27524-6_8","volume-title":"Specification of Behavioral Semantics in Object-Oriented Information Modeling","author":"G. T. Leavens","year":"1996","unstructured":"Gary T. Leavens. An overview of Larch\/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 121\u2013142. Kluwer Academic Publishers, Boston, 1996. An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011."},{"key":"8_CR33","unstructured":"Gary T. Leavens. Larch\/C++ Reference Manual. Version 5.41. Available in ftp:\/\/ftp.cs.iastate.edu\/pub\/larchc++\/lcpp.ps.gz or on the World Wide Web at the URL http:\/\/www.cs.iastate.edu\/~leavens\/larchc++.html, April 1999."},{"key":"8_CR34","unstructured":"Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06e, Iowa State University, Department of Computer Science, June 1999."},{"key":"8_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/BFb0030623","volume-title":"Theory and Practice of Software Development, 7th International Joint Conference CAAP\/FASE, Lille, France","author":"G. T. Leavens","year":"1997","unstructured":"Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. In Michel Bidoit and Max Dauchet, editors, TAPSOFT\u2019 97: Theory and Practice of Software Development, 7th International Joint Conference CAAP\/FASE, Lille, France, volume 1214 of Lecture Notes in Computer Science, pages 520\u2013534. Springer-Verlag, New York, N.Y., 1997."},{"key":"8_CR36","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/PL00003926","volume":"10","author":"G. T. Leavens","year":"1998","unstructured":"Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. Formal Aspects of Computing, 10:59\u201375, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"8_CR37","unstructured":"K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03."},{"issue":"6","key":"8_CR38","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Barbara Liskov and Jeannette Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811\u20131841, November 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Barbara Liskov and Jeannette M. Wing. Specifications and their use in defining subtypes. ACM SIGPLAN Notices, 28(10):16\u201328, October 1993. OOPSLA\u2019 93 Proceedings, Andreas Paepcke (editor).","DOI":"10.1145\/165854.165863"},{"key":"8_CR40","volume-title":"Texts and Monographs in Computer Science","author":"D. Luckham","year":"1990","unstructured":"David Luckham. Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, New York, N.Y., 1990."},{"issue":"2","key":"8_CR41","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/MS.1985.230345","volume":"2","author":"D. Luckham","year":"1985","unstructured":"David Luckham and FriedrichW. von Henke. An overview of anna-a specification language for Ada. IEEE Software, 2(2):9\u201323, March 1985.","journal-title":"IEEE Software"},{"key":"8_CR42","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, New York, N.Y., second edition, 1997.","edition":"second edition"},{"key":"8_CR43","volume-title":"Programming from Specifications: Second Edition","author":"C. Morgan","year":"1994","unstructured":"Carroll Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994."},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Carroll Morgan and Trevor Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, N.Y., 1994.","DOI":"10.1007\/978-1-4471-3273-8"},{"issue":"3","key":"8_CR45","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"Joseph M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287\u2013306, December 1987.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"8_CR46","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"Greg Nelson. A generalization of Dijkstra\u2019s calculus. ACM Transactions on Programming Languages and Systems, 11(4):517\u2013561, October 1989.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"8_CR47","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/190679.190681","volume":"19","author":"W. F. Ogden","year":"1994","unstructured":"William F. Ogden, Murali Sitaraman, Bruce W. Weide, and Stuart H. Zweben. Part I: The RESOLVE framework and discipline-a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4):23\u201328, Oct 1994.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"8_CR48","doi-asserted-by":"crossref","unstructured":"D. E. Perry. The Inscape environment. In Proceedings of the 11th International Conference on Software Engineering, pages 2\u201312, May 1989.","DOI":"10.1109\/ICSE.1989.714388"},{"key":"8_CR49","unstructured":"Arnd Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997."},{"issue":"1","key":"8_CR50","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/32.341844","volume":"21","author":"D. S. Rosenblum","year":"1995","unstructured":"David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19\u201331, January 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"8_CR51","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1142\/S0218194093000100","volume":"3","author":"M. Sitaraman","year":"1993","unstructured":"Murali Sitaraman, Lonnie R. Welch, and Douglas E. Harms. On specification of reusable software components. International Journal of Software Engineering and Knowledege Engineering, 3(2):207\u2013229, 1993.","journal-title":"International Journal of Software Engineering and Knowledege Engineering"},{"key":"8_CR52","volume-title":"International Series in Computer Science","author":". M. Spivey","year":"1992","unstructured":". Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, N.Y., second edition, 1992.","edition":"second edition"},{"key":"8_CR53","doi-asserted-by":"crossref","unstructured":"Susan Stepney, Rosalind Barden, and David Cooper, editors. Object Orientation in Z. Workshops in Computing. Springer-Verlag, Cambridge CB2 1LQ, UK, 1992.","DOI":"10.1007\/978-1-4471-3552-4_1"},{"key":"8_CR54","series-title":"Technical Report","volume-title":"Formal specification techniques for promoting software modularity, enhancing documentation, and testing specifications","author":"Y. M. Tan","year":"1994","unstructured":"Yang Meng Tan. Formal specification techniques for promoting software modularity, enhancing documentation, and testing specifications. Technical Report 619, Massachusetts Institute of Technology, Laboratory for Computer Science, 545 Technology Square, Cambridge, Mass., June 1994."},{"issue":"8","key":"8_CR55","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/185087.185106","volume":"29","author":"Y. M. Tan","year":"1994","unstructured":"Yang Meng Tan. Interface language for supporting programming styles. ACM SIGPLAN Notices, 29(8):74\u201383, August 1994. Proceedings of the Workshop on Interface Definition Languages.","journal-title":"ACM SIGPLAN Notices"},{"key":"8_CR56","series-title":"Kluwer International Series in Software Engineering","volume-title":"Formal Specification Techniques for Engineering Modular C Programs","author":"Y. M. Tan","year":"1995","unstructured":"Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs, volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers, Boston, 1995."},{"key":"8_CR57","doi-asserted-by":"crossref","unstructured":"Alan Wills. Specification in Fresco. In Stepney et al. [53], chapter 11, pages 127\u2013135.","DOI":"10.1007\/978-1-4471-3552-4_11"},{"issue":"1","key":"8_CR58","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"J. M. Wing","year":"1987","unstructured":"Jeannette M. Wing. Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems, 9(1):1\u201324, January 1987.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR59","unstructured":"Jeannette Marie Wing. A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science, 1983."},{"key":"8_CR60","unstructured":"Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science, 1996."}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T11:30:51Z","timestamp":1556969451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}