Unambiguous and precise software specification can not be achieved without some use of formal notation. Table-based specification techniques are both readable and convenient. They allow the representation of systems specifications in a very compact and yet precise manner. They scale to software systems, and they may be easily used even by people unfamiliar with the application domain. Additionally, the use of table-based notations makes it relatively easy to check for such properties as consistency and completeness. Among the table-based specification techniques discussed in the literature, the most popular are the Software Cost Reduction (SCR) method and tabular expressions. Both of these techniques are successfully used in practice to formally specify software requirements.;The second technique tabular expressions comprises a collection of cells, with each cell holding a single expression. The beauty of tabular expressions stems from both their visual structure and their concise representation of mathematical functions and relations. As a result, these expressions are suitable for use in every software engineering phase, from establishing requirements to completing final testing.;To successfully be used in practice, the specification techniques chosen should be supported by tools for creating, editing and transforming tables. Creating tools in the absence of reasonable formal semantics often results in failure. Formal semantics are also needed to compose and decompose tables in a modular way.;Although SCR has been used in many projects and organizations to specify software requirements, perhaps surprisingly, its semantics are not well defined. Specifically, the symbols used in this method are ambiguous, especially those that serve to denote SCR events. Further, the SCR method does not include either table composition or decomposition.;The Software Cost Reduction (SCR) method is a formal method for specifying the requirements of software systems that is based on tabular notation. SCR is used in a wide range of applications.;The tabular expressions technique was also lacking, though in different ways than SCR. A literature review revealed that the techniques applied to address the challenges inherent in tabular expressions composition have their own limitations.;The aim of this research, then, was to improve the semantics of both the SCR and the tabular expressions specification methods. To this end, SCR tables were converted into tabular expressions, as they have a rather precise semantics. Additionally, a new way to model the SCR events with first order logic is presented. Finally, a simpler way to define SCR events with propositional logic is proposed.;By improving the semantics of the two specification methods, numerous advantages are realized. These include increasing the readability of tables, and eliminating previously ambiguous symbols.;Moreover, improving the semantics enabled certain tasks to be carried out more easily, such as facilitating the verification and validation process and improving the toolset supporting the SCR method. In moving towards a richer semantics, this research allowed for the introduction of algebra for tabular expressions, as well as operators for tables composition and decomposition. Further, the research revealed the inherent power of tabular expressions. This was accomplished by composing a regression to demonstrate where tabular expressions get their power in specifying functions, relations and programs. An application of tabular expressions for three dimensions and higher is successfully presented. Next, a language and a structure for tabular expressions is proposed. Then, it is shown how tabular expressions could be represented by a lattice and by a vector space, respectively. Finally, the discussion considers the ways in which such an enhanced tabular expressions application could also be applied to other fields, such as software engineering and computer science.
展开▼
