Abstract
An important perquisite for verification of the correctness of software is the ability to write mathematically precise documents that can be read by practitioners and advanced users. Without such documents, we won't know what properties we should verify. Tabular expressions, in which predicate expressions may appear, have been found useful for this purpose. We frequently use partial functions in our tabular documentation. Conventional interpretations of expressions that describe predicates are not appropriate for our application because they do not deal with partial functions. Experience with this documentation has led us to choose a logic in which predicates are total but functions remain partial. We have found that this particular interpretation results in simpler expressions and is easily understood by practitioners.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Cheng, J. H. and C. B. Jones: 1991, ‘On the Usability of Logics Which Handle Partial Functions’, in C. Morgan and J. Woodcock (eds.),Proceedings of the Third Refinement Workshop, Springer-Verlag, Heidelberg.
Dijkstra, E. W.: 1976,A Discipline of Programrning, Prentice Hall, Englewood Cliffs NJ.
Farmer, W. M.: 1990, ‘A Partial Functions Version of Church's Simple Theory of Types’,The Journal of Symbolic Logic 55, 1269–1291.
Halmos, P. R.: 1960,Naive Set Theory, Van Nostrand Rheinhold, New York.
Heninger, K. L., J. W. Kallander, J. E. Shore, and D. L. Parnas: 1978, ‘Software Requirements for the A-7E Aircraft’,NRL Report 3876.
Heninger, K. L.: 1980, ‘Specifying Software Requirements for Complex Systems: New Techniques and Their Application’,IEEE Trans. Software Engineering,SE-6, 2–13.
Hester, S., D. L. Parnas, and D. F. Utter: 1981, ‘Using Documentation as a Software Design Medium’, inBell System Technical Journal.
Janicki, R.: 1995, ‘Towards a Formal Semantics of Tables’,Proceedings of the 17th International Conference on Software Engineering, Seattle WA, pp. 231–240.
Mendelson, E.: 1987,Introduction to Mathematical Logic 55, Third Edition, Wadsworth and Brooks, Pacific Grove California (USA).
Parnas, D. L.: 1992,Tabular Representation of Relations, CRL Report 260, McMaster University, TRIO (Telecommunications Research Institute of Ontario), p. 12.
Parnas, D. L., G. J. K. Asmis, and J. Madey: 1991, ‘Assessment of Safety-Critical Software in Nuclear Power Plants’,Nuclear Safety 32(2), 189–198.
Parnas, D. L. and J. Madey: 1995, ‘Functional Documentation for Computer Systems Engineering (Version 2)’, CRL Report 237, McMaster University, TRIO (Telecommunications Research Institute of Ontario), September 1991, p. 14. Revised version to appear inScience of Computer Programming (Elsevier).
Parnas, D. L., J. Madey, and M. Iglewski: 1994, ‘Precise Documentation of Well-Structured Programs’,IEEE Transactions on Software Engineering,20(12), 948–976.
Parnas, D. L.: 1994, ‘Mathematical Descriptions and Specification of Software’,Proceedings of IFIP World Congress 1994,1, 354–359.
Zucker, J. I.: 1993, ‘Normal and Inverted Function Tables’, CRL Report 265, McMaster University, Communications Research Laboratory, TRIO (Telecommunications Research Institute of Ontario), p. 15.
Zucker, J. I.: 1994, ‘Transformations of Normal and Inverted Function Tables’, CRL Report 291, McMaster University, Communications Research Laboratory, TRIO (Telecommunications Research Institute of Ontario), p. 26.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Parnas, D.L. A logic for describing, not verifying, software. Erkenntnis 43, 321–338 (1995). https://doi.org/10.1007/BF01135377
Issue Date:
DOI: https://doi.org/10.1007/BF01135377