{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:53:44Z","timestamp":1694624024685},"reference-count":12,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1997,7,1]],"date-time":"1997-07-01T00:00:00Z","timestamp":867715200000},"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":[[1997,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A commonly made criticism of formal methods is that they increase costs. Selective use of formal methods to define critical requirements can, however, lead to a significant decrease in lifecycle costs. In particular the economic and technical benefits of outsourcing the development of software can be fully realized and the cost of outsourcing slightly reduced by use of a formal specification. In this paper we describe a development in which a formal specification prepared by the customer formed part of the contract with the supplier. We conclude that this use of a formal specification can reduce risks and costs for all concerned and can help foster fruitful and co-operative relations in situations which are often fraught with confrontation.<\/jats:p>","DOI":"10.1007\/bf01211295","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T22:18:43Z","timestamp":1109369923000},"page":"349-358","source":"Crossref","is-referenced-by-count":6,"title":["Using a formal specification contractually"],"prefix":"10.1145","volume":"9","author":[{"given":"C.","family":"O'Halloran","sequence":"first","affiliation":[{"name":"DERA Malvern, WR14 3PS, Worcestershire, UK"}]},{"given":"R.","family":"Arthan","sequence":"additional","affiliation":[{"name":"LEMMA1, Twyford, Berks, UK"}]},{"given":"D.","family":"King","sequence":"additional","affiliation":[{"name":"Hoskyns Group plc, London, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Bramson B. D.: Tools for the specification design analysis and verification of software RSRE report 87005 1987."},{"key":"e_1_2_1_2_2_2","unstructured":"Eds. Stephen Brien John Nichols Z base standard \u2014 version 1.0. ZIP DTI\/IED project number 1639 . Deliverable D1.3.3 November 1992."},{"key":"e_1_2_1_2_3_2","unstructured":"Carr\u00e9 B. A. Jennings T. J. Maclennan F. J. Farrow P. F. and Garnsworthy P. F.: SPARK \u2014 The SPADE Ada Kernel (Edition 3.1). Program Validation Ltd."},{"key":"e_1_2_1_2_4_2","unstructured":"Granville R. J. and O'Halloran C.: Malpas IL (version 3.2) RSRE memorandum 3731 1986."},{"key":"e_1_2_1_2_5_2","unstructured":"Hewitt M. A.: Optimization of Prolog Generated from Z Specifications M.Sc Project Report 1992 Department of Computing Science University of Aberdeen."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Hewitt R. J. O'Halloran C. and Sennett C. T.: Experiences with PiZA an animator for Z in J. P. Bowen et al editors Proceedings ZUM'97 LNCS 1212 Springer April 1997.","DOI":"10.1007\/BFb0027282"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Knuth D. E.: Literate Programming Computer Journal Vol. 27 No. 2 1984","DOI":"10.1093\/comjnl\/27.2.97"},{"key":"e_1_2_1_2_8_2","unstructured":"Morgan C.: Programming from Specifications Prentice Hall 1990."},{"key":"e_1_2_1_2_9_2","unstructured":"O'Halloran C. M. Sennett C. T. and Smith A.: Refinement of Z to SPARK (Volumes 1 2 3) DRA 1994 http:\/\/daedalus.dra.hmg.gb\/hewitt\/swi\/swi.html."},{"key":"e_1_2_1_2_10_2","unstructured":"Program Validation Limited The formal semantics of SPARK March 1994 http:\/\/daedalus.dra.hmg.gb\/hewitt\/swi\/swi.html"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Sennett C. T.: Demonstrating the compliance of Ada programs with Z specifications Proceedings of the 5th Refinement Workshop London 8\u201310th January 1992. SpringerVerlag 1992.","DOI":"10.1007\/978-1-4471-3550-0_5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Ward N. J.: The static analysis of Safety-Critical Software using MALPAS in R. Genser et al editors Safety of Computer Control Systems 1989 (SAFECOMP'89) IFAC\/IFIP Workshop Pergamon Press Oxford.","DOI":"10.1016\/S1474-6670(17)52801-3"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211295.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211295\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:35Z","timestamp":1641482675000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,7]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1997,7]]}},"alternative-id":["10.1007\/BF01211295"],"URL":"https:\/\/doi.org\/10.1007\/bf01211295","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,7]]}}}