×

Defining the meaning of tabular mathematical expressions. (English) Zbl 1209.68126

Summary: Mathematical expressions in tabular form (also called “tabular expressions” or “tables”) have been shown to be useful for documenting and analysing software systems. They are usually easier to read than conventional mathematical expressions but are no less precise. They can be used wherever mathematical expressions are used. To avoid misunderstandings, and to support users with trustworthy tools, the meaning of these expressions must be fully defined.
This paper presents a new method for defining the meaning of tabular expressions. Each definition of an expression type names the expression’s constituents, and provides a restriction schema and one or more evaluation schemas. The restriction schema defines the class of well-formed expressions of the type. An evaluation schema maps a well-formed tabular expression of the type to a mathematical expression of a previously defined type. Since the meaning of conventional mathematical expressions is well known, describing an equivalent expression fully defines the meaning of a tabular expression.
In this approach, indexation is used to decouple the appearance of a tabular expression from its semantics. A tabular expression is an indexed set of grids; a grid is an indexed set of expressions. The expressions in a grid can be either conventional expressions or tabular expressions of a previously defined type.
Defining the meaning of a tabular expression in this way facilitates the building of tools that faithfully implement the semantics. The decoupling of syntax and semantics by means of indices overcomes some limitations of older approaches.
The method presented in the paper is illustrated by defining several previously known types of tabular expressions and some new ones. The use of the new model to build a suite of tools for the input, presentation, validation, evaluation, simplification, conversion and composition of tabular expressions is discussed.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N99 Theory of software

Software:

SCR
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] R.F. Abraham, Evaluating generalized tabular expressions. M.Eng. Thesis, McMaster University, 1997
[2] Baber, R.; Parnas, D. L.; Vilkomir, S.; Harrison, P.; O’connor, T.: Disciplined methods of software specifications: A case study, (2005)
[3] Desharnais, J.; Khedri, R.; Mili, A.: Interpretation of tabular expressions using arrays of relations, Studies in fuzziness and soft-computing 65, 3-14 (2001) · Zbl 1061.68536
[4] T. Fu, Structured Decision Table – Generalized Decision Table Conversion Tool, Technical Report SERG 380 [39], McMaster University Canada, 1999
[5] Halmos, P. R.: Naive set theory, (1987)
[6] Heitmeyer, C. L.: Software cost reduction, Encyclopedia of software engineering, two volumes (2002)
[7] C.L. Heitmeyer, R.D. Jeffords, Applying a formal requirements method to three NASA systems: Lessons learned, in: Proceedings of the 2007 IEEE Aerospace Conference, Big Sky, Montana, USA, March 2007
[8] K. Heninger, J. Kallander, D.L. Parnas, J. Shore, Software requirements for the A-7E aircraft, NRL Report 3876, November 1978, 523 p
[9] Heninger, K.: Specifying software requirements for complex systems: new techniques and their application, IEEE transactions on software engineering 6, No. 50 (1980)
[10] Hester, S. D.; Parnas, D. L.; Utter, D. F.: Using documentation as a software design medium, Bell system technical journal 60, No. 8, 1941-1977 (1981)
[11] R. Janicki, Towards a formal semantics of Parnas tables, in: Proc. of 17th International Conference on Software Engineering, Seattle, WA, 1995, pp. 231–240
[12] R. Janicki, On a formal semantics of tabular expressions, Technical Report CRL 355 [38], McMaster University, Canada, 1997 · Zbl 0971.68100
[13] Janicki, R.; Khedri, R.: On a formal semantics of tabular expressions, Science of computer programming 39, 189-213 (2001) · Zbl 0971.68100 · doi:10.1016/S0167-6423(00)00004-6
[14] Janicki, R.; Parnas, D. L.; Zucker, J.: Tabular representations in relational documents, Relational methods in computer science, 184-196 (1997) · Zbl 1114.68597
[15] Wolfram Kahl, Compositional syntax and semantics of tables, Technical Report SQRL 15 [40], Software Quality Research Laboratory, McMaster University Canada, 2003
[16] Mendelson, E.: Introduction to mathematical logic, (1987) · Zbl 0681.03001
[17] Parnas, D. L.; Asmis, G. J. K.; Madey, J.: Assessment of safety-critical software in nuclear power plants, Nuclear safety 32, No. 2 (1991)
[18] D.L. Parnas, Tabular representation of relations, Technical Report CRL 260 [38], McMaster University Canada, 1992
[19] Parnas, D. L.: Predicate logic for software engineering, IEEE transactions on software engineering 19, No. 9, 856-862 (1993)
[20] D.L. Parnas, Inspection of safety critical software using function tables, in: Proceedings of IFIP World Congress 1994, Volume III,. 1994, pp. 270–277. Reprinted as Chapter 19 in [40]
[21] Parnas, D. L.; Madey, J.; Iglewski, M.: Precise documentation of well-structured programs, IEEE transactions on software engineering 20, No. 12, 948-976 (1994)
[22] Parnas, D. L.; Kreyman, K.: Documenting requirements for software models of environmental phenomena, Oceanography 14, No. 1, 41-42 (2001)
[23] Parnas, D. L.; Madey, J.: Functional documentation for computer systems engineering, Science of computer programming 25, No. 1, 41-61 (1995)
[24] Parnas, D. L.; Peters, D. K.: An easily extensible toolset for tabular mathematical expressions, Lecture notes in computer science (LNCS) 1579, 345-359 (1999)
[25] Parnas, D. L.; Wang, Y.: Simulating the behaviour of software modules by trace rewriting systems, IEEE transactions of software engineering 19, No. 10, 750-759 (1994)
[26] D.L. Parnas, Y. Wang, The trace assertion method of module interface specification, Technical Report 89-261, Queen’s, Kingston, TRIO, October 1989, 39 p
[27] D.L. Parnas, J.E. Shore, D. Weiss, Abstract Types Defined as Classes of Variables, in: Proceedings Conference on Data: Abstraction, Definition, and Structure, Salt Lake City, March 1976, pp. 22–24. Reprinted in NRL Memorandum Report 7998, April 22, 1976, pp. 1–10. Reprinted as Chapter 11 in [41]
[28] Peters, D.; Parnas, D. L.: Using test oracles generated from program documentation, IEEE transactions on software engineering 24, No. 3, 161-173 (1998)
[29] Peters, D. K.; Parnas, D. L.: Requirements-based monitors for real-time systems, IEEE transactions on software engineering 28, No. 2, 146-158 (2002)
[30] C. Quinn, S.A. Vilkomir, D.L. Parnas, S. Kostic, Specification of software component requirements using the trace function method, in: Proceedings of the International Conference on Software Engineering Advances, ICSEA 2006, October 29–November 1, 2006, Tahiti, French Polynesia
[31] Shen, H.; Zucker, J. I.; Parnas, D. L.: Table transformation tools: why and how, , 3-11 (1996)
[32] H. Shen, Implementation of table inversion algorithms, CRL Report No. 315 [38], Telecommunications Research Institute of Ontario (TRIO), McMaster University, Hamilton, ON, Canada, December 1995, 96 p
[33] Software Engineering Research Group. Table tool system developer’s guide, CRL Report 339 [38], Telecommunications Research Institute of Ontario (TRIO), McMaster University, Hamilton, ON, January 1997
[34] Wassyng, L.; Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project, Lncs 2805, 133-153 (2003)
[35] Wilder, A.; Tucker, J. V.: Documenting computer systems using tables, (1996)
[36] Zucker, J. I.: Transformations of normal and inverted function tables, Formal aspects of computing 8, 679-705 (1996) · Zbl 0862.68075 · doi:10.1007/BF01213494
[37] J.I. Zucker, H. Shen, 1998, Table transformation: Theory and tools, McMaster University, Dept of Computing and Software, Report CAS 98-01; Also Communications Research Laboratory (CRL) Report 363 [38]
[38] McMaster CRL Reports, http://www.cas.mcmaster.ca/serg/crl_reports.html
[39] McMaster SERG Reports, http://www.cas.mcmaster.ca/serg/serg_reports.html
[40] McMaster SQRL Reports, http://www.cas.mcmaster.ca/sqrl/sqrl_reports.html
[41] , Software fundamentals: collected papers by david L. Parnas (2001)
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.