This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Supertotal Function Definition in Mathematics and Software Engineering
July 2000 (vol. 26 no. 7)
pp. 662-672
ASCII Text
x 
 
Raymond Boute, "Supertotal Function Definition in Mathematics and Software Engineering," IEEE Transactions on Software Engineering, vol. 26, no. 7, pp. 662-672, July, 2000.
 
 
BibTex
x
 
@article{ 10.1109/32.859534,
author = {Raymond Boute},
title = {Supertotal Function Definition in Mathematics and Software Engineering},
journal ={IEEE Transactions on Software Engineering},
volume = {26},
number = {7},
issn = {0098-5589},
year = {2000},
pages = {662-672},
doi = {http://doi.ieeecomputersociety.org/10.1109/32.859534},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Supertotal Function Definition in Mathematics and Software Engineering
IS - 7
SN - 0098-5589
SP662
EP672
EPD - 662-672
A1 - Raymond Boute,
PY - 2000
KW - Formal methods
KW - software specification
KW - predicate calculus
KW - calculational reasoning
KW - functional mathematics
KW - guarded formulas
KW - conditional expressions
KW - undefinedness
KW - type correctness
KW - subtyping.
VL - 26
JA - IEEE Transactions on Software Engineering
ER -
 

Abstract—In engineering (including computing), mathematics and logic, expressions can arise that contain function applications where the argument is outside the function's domain. Such a situation need not represent a conceptual error, for instance, in conditional expressions, but it is traditionally considered a type error. Various solutions can be found in the literature based on the notion of partial function and/or a distinguished value undefined. However, these have rather pervasive effects, complicating function definition, sacrificing convenient algebraic laws of logical operators and/or Leibniz's rule, one of the most valuable assets in formal reasoning (especially in the calculational style). Other solutions have in common the realization that well-structured mathematical arguments are always guarded by conditions and that the value of $A \Rightarrow B$ is not affected by domain violations in $B$ in case $\neg A$. These solutions preserve Leibniz's rule and the standard meaning of the logical operators. In this second category, we propose the simplest possible solution, called supertotal function definition, and consisting of assigning the value false (or 0, depending on the preferred formalism) to any function application where the argument is outside the domain. This approach assumes the notion of function with which a domain is associated as a part of its specification. Ramifications regarding formal reasoning, use in software engineering (such as Parnas's predicate calculus) and in mathematical formulation in general are discussed. The proposed solution justifies formal reasoning as usual, but with increased freedom in expressions regarding types of function arguments. Hence, it can be adopted in existing formalisms with very minor changes to the latter. As a bonus, this discussion includes a very simple new view on conditional expressions, yielding unusually powerful and convenient calculational properties. Finally, differences and advantages w.r.t. other approaches are pointed out.

[1] D.L. Parnas, “Predicate Logic for Software Engineering,” IEEE Trans Software Eng., vol. 19, no. 9 pp. 856–862 Sept. 1993.
[2] W.F. Farmer, “A Partial Functions Version of Church's Simple Theory of Types,” J. Symbolic Logic, pp. 1269–1291, Sep. 1990.
[3] J.H. Cheng and C.B. Jones, “On the Usability of Logics which Handle Partial Functions,” Proc. Third Refinement Workshop, C. Morgan and J. Woodcock, eds., Springer-Verlag, pp. 51–69, 1991.
[4] D. Gries, “Foundations for Calculational Logic,” M. Broy and B. Schieder Eds., Mathematical Methods in Program Development, pp. 83-126, Springer NATO ASI Series F158, 1997.
[5] E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics. Springer-Verlag, 1989.
[6] D. Gries and F.B. Schneider, A Logical Approach to Discrete Math, Berlin: Springer-Verlag, 1993.
[7] R. Boute, “Algorithms for Combinational Fault Equivalence using LISP,” Technical Note No. 9, Digital Systems Laboratory, Stanford Univ., Sept. 1971
[8] E.W. Dijkstra, A Discipline of Programming.Englewood Cliffs, N.J.: Prentice Hall, 1976.
[9] M. Levin, “Mathematical Logic for Computer Scientists,” Report MAC TR-131, Massachusetts Inst. of Tech nology, June 1974.
[10] R.T. Boute, “Fundamentals of Hardware Description Languages and Declarative Languages,” Fundamentals and Standards in Hardware Description Languages, pp. 3-38, J.P. Mermet ed., Kluwer Academic, 1993.
[11] R.T. Boute, “Funmath illustrated: A Declarative Formalism and Application Examples,” Declarative Systems Series No. 1, Computing Science Inst., Univ. of Nijmegen, July 1993.
[12] S. Lang, “Undergraduate Analysis,” Berlin, 1983.
[13] E. Mendelson, Introduction to Mathematical Logic, second edition. D. Van Nostrand. (author: year published?)
[14] B. Meyer, Introduction to the Theory of Programming Languages, Prentice Hall, Hemel Hempstead, U.K., 1990.
[15] A. Syropoulos and A. Karakos, “Bottom in the Imperative World,” ACM SIGPLAN Notices, vol. 30, no. 5, pp. 18–20, May 1995.
[16] A. Bijlsma, “Semantics of Quasi-Boolean Expressions,” Beauty Is Our Business–A Birthday Salute to Edsger W. Dijkstra, W.H.J. Feyen, A.J.M. van Gasteren, D. Gries, and J. Misra, eds., pp. 27–35 New York: Springer-Verlag, 1990
[17] J.A Bergstra, I. Bethke, and P.H. Rodenburg, “A Propositional Logic with 4 Values: True, False, Divergent, and Meaningless,” Programming Research Group Technical Report P9406., Univ. of Amsterdam, 1994.
[18] J.A Bergstra and A. Ponse, “Process Algebra with Four-Valued Logic,” Programming Research Group Technical Report P9724, Univ. of Amsterdam, 1997
[19] E.B. Eichelberger, “Hazard Detection in Combinational and Sequential Circuits,” IBM J. on Res. and Dev., pp.90–99, Mar. 1965.
[20] A. Zamfirescu, “Logic and Arithmetic in Hardware Description Languages,” Fundamentals and Standards in Hardware Description Languages, NATO ASI Series, pp. 79–107 J.P. Mermet, ed., Dordrecht: Kluwer Academic, 1993.
[21] R. Boute, “Conditionals, Guards and Inverses in Funmath and Comma,” Tech. Note, School of Math. and Informatics, Univ. of Nijmegen, Netherlands, 1990.
[22] F. van den Beuken, “A Functional Approach to Syntax and Typing,” Ph.D. Thesis, School of Math. and Informatics, Univ. of Nijmegen, Netherlands, 1997.
[23] D.S Scott, “Existence and Description in Formal Logic,” Bertrand Russell, Philosopher of the Century, pp. 51–69, R. Schoenman, ed., St. Leonards: Allen and Unwin, 1967.
[24] E.C. Hehner, “From Boolean Algebra to Unified Algebra,” Internal Report, Univ. of Toronto, June 1997.
[25] C.B. Jones and C.A. Middelburg, “A Typed Logic of Partial Functions Reconstructed Classically,” Acta Informatica vol. 31 pp. 399–430, 1994.
[26] C.B. Jones, “Partial Functions and Logics: A Warning,” Information Processing Letters 54, pp. 65–68, 1995.
[27] L. Lamport and L.C. Paulson, “Should Your Specification Language Be Typed?,” SRC Research Report 147, Digital Equip. Corp., May 1997.
[28] J. Rushby, S. Owre, and N. Shankar, “Subtypes for Specifications: Predicate Subtyping in PVS,” IEEE Trans. Software Eng., vol. 24, no. 9, pp. 709–720, Sept. 1998.
[29] R. Guym, “Wat's Left?,” Math Horizons, pp. 57–57, Apr. 1998.

Index Terms:
Formal methods, software specification, predicate calculus, calculational reasoning, functional mathematics, guarded formulas, conditional expressions, undefinedness, type correctness, subtyping.
Citation:
Raymond Boute, "Supertotal Function Definition in Mathematics and Software Engineering," IEEE Transactions on Software Engineering, vol. 26, no. 7, pp. 662-672, July 2000, doi:10.1109/32.859534
Usage of this product signifies your acceptance of the Terms of Use.