{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:42:45Z","timestamp":1742388165595},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1998,9]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The interface specification of a procedure describes the procedure's behaviour using pre- and postconditions. These pre- and postconditions are written using various functions. If some of these functions are partial, or underspecified, then the procedure specification may not be well-defined.<\/jats:p>\n          <jats:p>We show how to write pre- and postcondition specifications that avoid such problems, by having the precondition \u201cprotect\u201d the postcondition from the effects of partiality and underspecification. We formalize the notion of protection from partiality in the context of specification languages like VDM-SL and COLD-K. We also formalize the notion of protection from underspecification for the Larch family of specification languages, and for Larch show how one can prove that a procedure specification is protected from the effects of underspecification.<\/jats:p>","DOI":"10.1007\/pl00003926","type":"journal-article","created":{"date-parts":[[2006,4,10]],"date-time":"2006-04-10T10:55:55Z","timestamp":1144666555000},"page":"59-75","source":"Crossref","is-referenced-by-count":10,"title":["Protective Interface Specifications"],"prefix":"10.1145","volume":"10","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[{"name":"Department of Computer Science, Iowa State University, Ames, IA, USA, , , , , , US"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeannette M.","family":"Wing","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA, , , , , , US"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"et al.: Information technology programming languages - VDM-SL: First committee draft standard CD1387-1. Document ISO\/IEC JTC1\/SC22\/WG19 N-20","author":"Andrews D. J.","year":"1993"},{"issue":"3","key":"p_2","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/BF00264250","article-title":"A logic covering undefinedness in program proofs","volume":"21","author":"Barringer H.","year":"1984","journal-title":"Acta Informatica"},{"key":"p_3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-2033-9","volume-title":"Proof in VDM: A Practitioner\u2019s Guide","author":"Bicarregui J.","year":"1994"},{"key":"p_4","first-page":"27","volume-title":"W. H. J. Feijen et al.","author":"Bij","year":"1990"},{"key":"p_5","first-page":"199","article-title":"The clean termination of iterative programs","volume":"16","author":"Bli","year":"1981","journal-title":"Acta Informatica"},{"key":"p_6","first-page":"387","article-title":"Three-valued predicates for software specification and validation","author":"Bli","year":"1991","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"p_7","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF00625280","article-title":"Partial abstract types","volume":"18","author":"Br","year":"1982","journal-title":"Acta Informatica"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/BF00289066","article-title":"The clean termination of Pascal programs","volume":"11","author":"Co","year":"1979","journal-title":"Acta Informatica"},{"key":"p_9","first-page":"51","volume-title":"Proceedings of the Third Refinement Workshop, Workshops in Computing Series","author":"Ch","year":"1990"},{"key":"p_10","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Formal Specification and Design","author":"Fe","year":"1992"},{"key":"p_11","doi-asserted-by":"crossref","unstructured":"[GCD95] \n      Gogolla M. Conrad S. Denker G. Herzig R. Vlachantonis N.\n     and \n      Ehrig\n      . \n      H.\n  : \n  TROLL light - the language and its development environment\n  . In Manfred Broy and Stefan J\u00e4hnichen editors KORSO\n  : Methods Languages and Tools for the Construction of Correct Software volume \n  1009\n   of \n  Lecture Notes in Computer Science pages \n  205\n  -\n  220\n  . \n  Springer-Verlag New York NY 1995\n  .","DOI":"10.1007\/BFb0015463"},{"key":"p_12","first-page":"105","volume-title":"Conference record of the Fifth Annual ACM Symposium on Principles of Programming Languages","author":"Ger","year":"1978"},{"issue":"6","key":"p_13","doi-asserted-by":"crossref","first-page":"1044","DOI":"10.1109\/32.58789","article-title":"Debugging Larch Shared Language specifications","volume":"16","author":"Garland S. J.","year":"1990","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag J. V.","year":"1993"},{"key":"p_16","first-page":"366","volume-title":"Computer Science Today: Recent Trends and Developments, number 1000 in Lecture Notes in Computer Science","author":"Gr D.","year":"1995"},{"key":"p_17","volume-title":"editor","author":"Hay","year":"1993"},{"issue":"5","key":"p_18","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/BF01178666","article-title":"A typed logic of partial functions reconstructed classically","volume":"31","author":"Jo","year":"1994","journal-title":"Acta Informatica"},{"key":"p_19","series-title":"International Series in Computer Science","volume-title":": Systematic Software Development Using VDM","author":"Jon","year":"1990"},{"issue":"2","key":"p_20","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(95)00042-B","article-title":"Partial functions and logics: A warning","volume":"54","author":"Jon","year":"1995","journal-title":"Information Processing Letters"},{"key":"p_21","doi-asserted-by":"crossref","first-page":"411","DOI":"10.3233\/FI-1991-14403","article-title":"A three-valued logic for software specification and validation","author":"Konikowska B.","year":"1991","journal-title":"Fundamenta Informaticae"},{"key":"p_22","volume-title":"October","author":"Lea","year":"1997"},{"key":"p_23","volume-title":"Object-oriented Software Construction","author":"Mey","year":"1988"},{"issue":"2","key":"p_24","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","article-title":"Formal verification for faulttolerant architectures: Prolegomena to the design of PVS","volume":"21","author":"Owre S.","year":"1995","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"p_25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/190679.190681","article-title":"Part I: The RESOLVE framework and discipline - a research synopsis","volume":"19","author":"Ogden W. F.","year":"1994","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"p_27","series-title":"International Series in Computer Science","volume-title":": The Z Notation: A Reference Manual","author":"Spi","year":"1992"},{"key":"p_28","doi-asserted-by":"crossref","unstructured":"[WDC95] \n      Wolter U. Didrich\n      K. Cornelius\n      F. Klar M. R.\n      Wess\u00e4ly and \n      H.\n      Ehrig\n  .: \n  How to cope with the spectrum of spectrum\n  . In Manfred Broy and Stefan J\u00e4hnichen editors KORSO\n  : Methods Languages and Tools for the Construction of Correct Software volume \n  1009\n   of \n  Lecture Notes in Computer Science pages \n  173\n  -\n  189\n  . \n  Springer-Verlag New York NY 1995\n  .","DOI":"10.1007\/BFb0015461"},{"key":"p_30","volume-title":"April","author":"Wo","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/PL00003926.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/PL00003926\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/PL00003926","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:29:27Z","timestamp":1641482967000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/PL00003926"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,9]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,9]]}},"alternative-id":["10.1007\/PL00003926"],"URL":"https:\/\/doi.org\/10.1007\/pl00003926","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,9]]}}}