4.1 Article

Defining the meaning of tabular mathematical expressions

Journal

SCIENCE OF COMPUTER PROGRAMMING
Volume 75, Issue 11, Pages 980-1000

Publisher

ELSEVIER SCIENCE BV
DOI: 10.1016/j.scico.2009.12.009

Keywords

Tabular expressions; Software documentation; Mathematical documentation; Expression semantics; Software engineering

Funding

  1. Science Foundation Ireland
  2. China 863 High-tech Research and Development Program [2007AA01Z123]

Ask authors/readers for more resources

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. (C) 2009 Elsevier B.V. All rights reserved.

Authors

I am an author on this paper
Click your name to claim this paper and add it to your profile.

Reviews

Primary Rating

4.1
Not enough ratings

Secondary Ratings

Novelty
-
Significance
-
Scientific rigor
-
Rate this paper

Recommended

No Data Available
Article Computer Science, Software Engineering

A formal approach for the correct deployment of cloud applications

Amel Mammar, Meriem Belguidoum, Saddam Hocine Hiba

Summary: This paper introduces a formal EVENT-B-based approach for modeling and verifying the deployment of component-based applications. By gradually refining an abstract model, a precise specification is built, and mathematical reasoning is used to prove its correctness. The presented approach validates the deployment in a cloud environment using PROB and ensures the construction of a correct system that meets the constraints.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Enhancing test reuse with GUI events deduplication and adaptive semantic matching

Shuqi Liu, Yu Zhou, Longbing Ji, Tingting Han, Taolue Chen

Summary: In this paper, we propose a framework that combines GUI events deduplication with an adaptive semantic matching strategy to enhance the usability of reused tests. Experimental evaluation demonstrates that the framework improves widget mapping performance, significantly reduces event redundancy, and reduces the manual effort of creating tests for similar applications.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

A method of test case set generation in the commutativity test of reduce functions

Xiangyu Mu, Lei Liu, Peng Zhang, Jingyao Li, Hui Li

Summary: The aim of this study is to reduce the size of the test case set required to detect the commutativity problem of the reduce function. By determining the pattern of the function and selecting corresponding test cases, the proposed test case generation strategy can achieve the same accuracy with a smaller test case set. It has been shown to be effective and has a high recall rate.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

An industrial experience report on model-based, AI-enabled proposal development for an RFP/RFI

Padmalata Nistala, Asha Rajbhoj, Vinay Kulkarni, Sapphire Noronha, Ankit Joshi

Summary: This paper presents an automated proposal development approach using a combination of model-based and AI-enabled techniques, and discusses the successful deployment and user feedback of the system.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Translation certification for smart contracts

Jacco O. G. Krijnen, Manuel M. T. Chakravarty, Gabriele Keller, Wouter Swierstra

Summary: Compiler correctness is a long-standing problem, and it becomes more significant with the rise of smart contracts on blockchains. A translation certification framework can address the trust issue for low-level code on the blockchain, allowing users to have confidence in the compilation process of smart contracts.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

OnTrack: Reflecting on domain specific formal methods for railway designs

Phillip James, Faron Moller, Filippos Pantekis

Summary: OnTrack is a tool that supports railway verification workflows using model driven engineering frameworks, allowing railway engineers to interact with verification procedures through encapsulating formal methods.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Generating C: Heterogeneous metaprogramming system description

Oleg Kiselyov

Summary: Heterogeneous metaprogramming systems leverage higher-level host languages to generate lower-level object language code, enabling faster production of high-performant code with correctness guarantees. This paper presents two systems with OCaml as the host language and C as the object language, discussing their implementation and applications.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Reasoning about logical systems in the Coq proof assistant

Conor Reynolds, Rosemary Monahan

Summary: This paper provides a detailed approach to formalize a fragment of the theory of institutions in the Coq proof assistant. The approach is illustrated and evaluated by instantiating the framework with specific institution examples.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Stochastic formal model of PI3K/mTOR pathway in Alzheimer's disease for drug repurposing: An evaluation of rapamycin, LY294002, and NVP-BEZ235

Herbert Rausch Fernandes, Giovanni Freitas Gomes, Antonio Carlos Pinheiro de Oliveira, Sergio Vale Aguiar Campos

Summary: Alzheimer's disease is a common form of dementia with no effective drug treatment available. In this study, a statistical model checking approach was used to analyze protein and drug interactions and evaluate the effects of different drugs on the components contributing to Alzheimer's disease. The results showed that rapamycin could slow down the biological process causing neuronal death, while LY294002 and NVP-BEZ235 may increase tau phosphorylation. These findings provide important insights for the scientific community and raise awareness about potential side effects of PI3K inhibitor drugs.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Denotational and operational semantics for interaction languages: Application to trace analysis

Erwan Mahe, Christophe Gaston, Pascale Le Gall

Summary: This paper presents an Interaction Language to encode Sequence Diagrams (SD) and associates it with three different formal semantics. This allows for direct formal verification of SD, while preserving traceability of SD concepts and executed actions, and addressing the translation of problematic operators.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

DescribeML: A dataset description tool for machine learning

Joan Giner-Miguelez, Abel Gomez, Jordi Cabot

Summary: Datasets are crucial for training and evaluating machine learning models, but they can also lead to undesirable behaviors like biased predictions. To tackle this issue, the machine learning community suggests adopting consistent guidelines for dataset descriptions. However, these guidelines rely on natural language descriptions, which hinder automated computation and analysis. To overcome this, we present DescribeML, a language engineering tool that provides precise, structured descriptions of machine learning datasets, including their composition, provenance, and social concerns.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

An iterative approach for model-based requirements engineering in large collaborative projects: A detailed experience report

Andrey Sadovykh, Bilal Said, Dragos Truscan, Hugo Bruneliere

Summary: In this paper, the authors report on their 7 years of practical experience with an iterative Model-based Requirements Engineering (MBRE) approach and language in five large European collaborative projects. They demonstrate through significant data sets that this model-based approach provides interesting benefits in terms of scalability, heterogeneity, adaptability, traceability, automation, consistency and quality, and usefulness or usability. Concrete examples from these projects are provided to illustrate the application of the MBRE approach and language, and the authors discuss the general benefits and limitations of using such an approach, as well as the lessons learned over the years.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

Exploring complex models with picto web

Alfa Yohannis, Dimitris Kolovos, Antonio Garcia-Dominguez

Summary: Picto Web is a multi-tenant web-based tool that allows exploration of complex models by transforming them into various transient web-based views using rule-based transformations. It uses a lazy view computation approach to efficiently support large models and complex transformations, and includes monitoring and push notification facilities for automatic recomputation of views and updated delivery to clients.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

GaMoVR: Gamification-based UML learning environment in virtual reality

Enes Yigitbas, Maximilian Schmidt, Antonio Bucchiarone, Sebastian Gottschalk, Gregor Engels

Summary: UML has become a popular modeling language used in computer science courses, and various interactive learning applications have been developed to improve student engagement and learning outcomes. However, these applications have not successfully created immersive environments for students. Therefore, this study introduces GaMoVR, a VR-based and gamified learning environment, which provides an interactive and fun learning experience for students learning about UML modeling.

SCIENCE OF COMPUTER PROGRAMMING (2024)

Article Computer Science, Software Engineering

How accessibility affects other quality attributes of software? A case study of GitHub

Yaxin Zhao, Lina Gong, Wenhua Yang, Yu Zhou

Summary: Accessible design aims to enable as many people as possible to access software products and services. This study investigates the interaction between accessibility issues and other factors affecting software performance. By analyzing a large number of accessibility issues, the study reveals the characteristics of these issues and their relationship with software quality attributes.

SCIENCE OF COMPUTER PROGRAMMING (2024)