--- abstract: 'Undefined terms involving the application of partial functions and operators are common in program specifications and in discharging proof obligations that arise in design. One way of reasoning about partial functions with classical First-order Predicate Calculus (FoPC) is to use a non-strict equality notion so as to insulate logical operators from undefined operands. An alternative approach is to work only with strict (weak) equality but use an alternative Logic of Partial Functions (LPF)—a logic in which the “Law of the Excluded Middle” does not hold. This paper explores the relationships between the theorems that can be proved in the two approaches. The main result is that theorems in LPF using weak equality can be straightforwardly translated into ones that are true in FoPC; translation in the other direction results, in general, in more complicated expressions but in many cases these can be readily simplified. Such results are important if the laudable move towards interworking of formal methods tools is to be sound.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: John.Fitzgerald@ncl.ac.uk copyright_holders: [] corp_creators: [] creators_id: - John.Fitzgerald@ncl.ac.uk - Cliff.Jones@ncl.ac.uk creators_name: - family: Fitzgerald given: John S honourific: '' lineage: '' - family: Jones given: Cliff B honourific: '' lineage: '' data_type: ~ date: 2008-07 date_type: published datestamp: 2008-08-06 19:47:20 department: ~ dir: disk0/00/00/00/29 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 29 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: /style/images/fileicons/application_pdf.png;/29/1/final.pdf full_text_status: public funders: - EC FP7 - EPSRC (UK) id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-04-19 15:05:50 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: 3-4 official_url: http://www.elsevier.com/wps/find/journaldescription.cws_home/505612/description?navopenmenu=-2 output_media: ~ pagerange: 128-132 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: - EC FP7 Deploy - EPSRC TrAmS publication: Information Processing Letters publisher: Elsevier refereed: TRUE referencetext: ".-R. Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press (1996).\r\n\r\nH. Barringer, J.H. Cheng and C.B. Jones, A logic covering undefinedness in program proofs, Acta Informatica 21 (1984), pp. 251–269. \r\n\r\nJ. Bicarregui, J. Fitzgerald, P. Lindsay, R. Moore and B. Ritchie, Proof in VDM: A Practitioner's Guide, FACIT, Springer-Verlag (1994) ISBN 3-540-19813-X.\r\n\r\nS.R. Blamey, Partial valued logic, PhD thesis, Oxford University, 1980.\r\n\r\nS. Blamey, Partial logic. In: D. Gabbay and F. Guenthuer, Editors, Handbook of Philosophical Logic vol. III, Reidel (1986) (Chapter 1).\r\n\r\nJ.H. Cheng, A logic for partial functions, PhD thesis, University of Manchester, 1986.\r\n\r\nJ.H. Cheng and C.B. Jones, On the usability of logics which handle partial functions. In: C. Morgan and J.C.P. Woodcock, Editors, 3rd Refinement Workshop, Springer-Verlag (1991), pp. 51–69.\r\n\r\nW.M. Farmer and J.D. Guttman, A set theory with support for partial functions, Studia Logica 66 (1) (2000), pp. 59–78. \r\n\r\nJ.S. Fitzgerald, The typed logic of partial functions and the Vienna development method. In: D. Bjørner and M.C. Henson, Editors, Logics of Specification Languages, EATCS Texts in Theoretical Computer Science, Springer (2007), pp. 427–461.\r\n\r\nJ. Fitzgerald and P.G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development, Cambridge University Press (1998).\r\n\r\nIn: I. Hayes, Editor, Specification Case Studies (second ed.), Prentice-Hall International (1993).\r\n\r\nC.B. Jones, K.D. Jones, P.A. Lindsay and R. Moore, mural: A Formal Development Support System, Springer-Verlag (1991) ISBN 3-540-19651-X.\r\n\r\nC.B. Jones and C.A. Middelburg, A typed logic of partial functions reconstructed classically, Acta Informatica 31 (5) (1994), pp. 399–430. MathSciNet | Full Text via \r\n\r\nC.B. Jones, Systematic Software Development using VDM (second ed.), Prentice-Hall International (1990) ISBN 0-13-880733-7.\r\n\r\nC.B. Jones, Reasoning about partial functions in the formal development of programs, Electronic Notes in Theoretical Computer Science 145 (January 2006), pp. 3–25.\r\n\r\nC. Jones, P. O'Hearn and J. Woodcock, Verified software: a grand challenge, IEEE Computer 39 (4) (2006), pp. 93–95. \r\n\r\nS.C. Kleene, Mathematical Logic, Wiley (1967).\r\n\r\nD. Prawitz, Natural Deduction: A Proof-Theoretical Study, Dover Publications (1965).\r\n" related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 19 series: ~ skill_areas: [] source: ~ status_changed: 2008-08-06 19:47:20 subjects: - deploy_method_proof - Proof succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: The connection between two ways of reasoning about partial functions type: article userid: 11 volume: 107