Abstract
This paper gives a comprehensive description of a typed version of the
logic known as LPF.
This logic is basic to formal specification and verified design in
the software development method VDM.
If appropriately extended to deal with recursively defined functions,
the data types used in VDM, etc., it gives the VDM notation and its
associated rules of reasoning.
The paper provides an overview of the needed extensions and examines
some of them in detail.
It is shown how this non-classical logic -- and the extensions --
can be reconstructed classically by embeddings into classical infinitary
logic.
View-only version of article
Preprint available here.