A typed logic of partial functions reconstructed classically (Q1338893)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A typed logic of partial functions reconstructed classically |
scientific article |
Statements
A typed logic of partial functions reconstructed classically (English)
0 references
24 January 1995
0 references
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 nonclassical logic -- and the extensions -- can be reconstructed classically by embeddings into classical infinitary logic.
0 references
logic LPF
0 references
formal specification
0 references
verified design
0 references
software development method VDM
0 references
embeddings into classical infinitary logic
0 references