×

A logic covering undefinedness in program proofs. (English) Zbl 0534.68024

There is a growing literature on proving that programs satisfy their specifications. Most methods employ propositional and predicate calculus. Such logical systems do not reflect the possibility of ”undefined values”. However, recursive definition often results in partial functions and iteration gives rise to programs that may fail to terminate for some inputs. This paper provides and demonstrates a logic in which the logical operators give defined results even if no value is known for some of their operands. It is claimed that this logical system is useful in program proofs.

MSC:

68Q65 Abstract data types; algebraic specification
03B60 Other nonclassical logic
68N01 General topics in the theory of software

Software:

LCF
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial, J.R.: Formal Programming. Privately circulated, March 1982
[2] Abrial, J.R.: A Theoretical Foundation to Formal Programming. Privately circulated, May 1982
[3] Bird, R.: Programs and Machines. New York: John Wiley, 1976 · Zbl 0357.68006
[4] Bjorner, D., Jones, C.B.: Formal Specification and Software Development. New York: Prentice-Hall, 1982 · Zbl 0525.68001
[5] Blamey, S.R.: Partial-Valued Logic. Ph.D. Thesis, Oxford University, 1980 · Zbl 0875.03023
[6] Blamey, S.R.: Partial Logic. In: Handbook of Philosophical Logic. (To appear) · Zbl 0875.03023
[7] Broy, M., Wirsing, M.: Partial Abstract Types. Acta Informat. 18, 47-64 (1982) · Zbl 0494.68020 · doi:10.1007/BF00625280
[8] Constable, R.L., O’Donnell, M.J.: A Programming Logic. Cambridge, MA: Winthrop Publishers, 1978
[9] Constable, R.L., Johnson, S.D., Eichenlaub, C.D.: An Introduction to the PL/CV2 Programming Logic. Berlin, Heidelberg, New York: Springer 1982 · Zbl 0496.68008
[10] Constable, R.L.: Partial functions in Constructive Formal Theories. Lecture Notes in Computer Science, Vol. 145. Berlin, Heidelberg, New York: Springer, 1983 · Zbl 0505.03027
[11] Dijkstra, E.W.: A Discipline of Programming. New York: Prentice-Hall, 1976 · Zbl 0368.68005
[12] Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, Vol. 78. Berlin, Heidelberg, New York: Springer, 1979 · Zbl 0421.68039
[13] Gries, D.: Science of Programming. Berlin, Heidelberg, New York: Springer, 1981 · Zbl 0472.68003
[14] Haack, S.: Deviant Logic. Cambridge: Cambridge University Press, 1974 · Zbl 0288.02007
[15] Haack, S.: Philosophy of Logics. Cambridge: Cambridge University Press, 1978 · Zbl 1005.03002
[16] Hoogewijs, A.: On a Formalization of the Non-definedness Notion. Z. Math. Logik 25, 213-221 (1979) · Zbl 0415.03019 · doi:10.1002/malq.19790251304
[17] Jones, C.B.: Formal Development of Correct Algorithms: An Example Based on Earley’s Recognizer. SIGPLAN 7, (1972)
[18] Jones, C.B.: Software Development: A Rigorous Approach. London: Prentice-Hall, 1980 · Zbl 0424.68019
[19] Jones, C.B.: Systematic Program Development. Talk given at CWI Amsterdam December 1983. (In press)
[20] Kleene, S.C.: Introduction to Metamathematics. Princeton: Van Nostrand, 1952 · Zbl 0047.00703
[21] Kleene, S.C.: Mathematical Logic. New York: John Wiley, 1967 · Zbl 0149.24309
[22] Koletsos, G.: Sequent Calculus and Partial Logic. M.Sc. Thesis, Manchester University, 1976
[23] Lucas, P., Walk, K.: On the Formal Description of P1/I. Ann. Rev. Automatic Progr. 6, 105-182 (1969) · Zbl 0217.53502 · doi:10.1016/0066-4138(69)90005-6
[24] McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Computer Programming and Formal Systems. P. Braffort, D. Hirschberg (eds.). Amsterdam: North-Holland, 1967
[25] Manna, Z.: Mathematical Theory of computation. New York: McGraw Hill, 1974 · Zbl 0353.68066
[26] Owe, O.: Program Reasoning Based on a Logic for Partial Functions. Privately circulated, 1982
[27] Plotkin, G.D.: Types and Partial Functions. Seminar, University of Manchester, 1984 · Zbl 0595.03027
[28] Prawitz, D.: Natural Deduction. Stockholm: Almgrist and Wiksell, 1965
[29] Rescher, N.: Many-valued Logic. New York: McGraw Hill, 1969 · Zbl 0248.02023
[30] Scott, D.S.: Combinators and Classes. In: Lecture Notes in Computer Science, Vol. 37. Böhm, C. (ed.). Berlin, Heidelberg, New York: Springer, 1975 · Zbl 0342.02018
[31] Scott, D.S.: Identity and Existence in Intuitionistic Logic. In: Lecture Notes in Mathematics, Vol.735. Berlin, Heidelberg, New York: Springer, 1979 · Zbl 0418.03016
[32] Wang, H.: The Calculus of Partial Predicates and Its Extension to Set Theory I. Math. Logik 7, 283-288 (1961) · Zbl 0124.24604 · doi:10.1002/malq.19610071705
[33] Woodruff, P.: Logic and Truth-Value Gaps in Philosophical Problems in Logic. Lambert, K. (ed.). Reidel, 1970 · Zbl 0194.30702
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.