• DocumentCode
    1370707
  • Title

    Supertotal function definition in mathematics and software engineering

  • Author

    Boute, Raymond

  • Author_Institution
    INTEC, Ghent Univ., Belgium
  • Volume
    26
  • Issue
    7
  • fYear
    2000
  • fDate
    7/1/2000 12:00:00 AM
  • Firstpage
    662
  • Lastpage
    672
  • 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⇒B is not affected by domain violations in B in case-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
  • Keywords
    formal specification; calculational reasoning; conditional expressions; formal methods; function definition; functional mathematics; guarded formulas; mathematics; predicate calculus; software engineering; software specification; subtyping; type correctness; undefinedness; Application software; Calculus; Logic; Mathematics; Software engineering; Software standards;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.859534
  • Filename
    859534