Added entries UNIVERSITY OF NEWCASTLE UPON TYNE

Decisions about the logic underpinning a formal specification language have important consequences for the utility of the formalism. This paper describes the major features of the typed Logic of Partial Functions~(LPF) as it has been implemented in support of the Vienna Development Method's Specification Language, VDM-SL. It compares attempts to realise the logic in different environments: a user-centred proof support tool, a specification interpreter and an automated proof tool. Future directions in integrated proof support for the language are suggested. © 2006 University of Newcastle upon Tyne. Printed and published by the University of Newcastle upon Tyne