GraphRedex: Look at your research. (3rd March 2021)

• Record Type: Journal Article
• Authors: Gurdeep Singh, Robbert; Scholliers, Christophe
• Is Part Of: Software, practice & experience. Volume 51:Number 6(2021)
• Page Start: 1322
• Page End: 1351
• Publication Date: 2021-03-03
• Subjects: operational semantics -- PLT Redex -- semantics engineering -- state explosion -- tooling -- visualization; Computer software -- Periodicals; Computer programming -- Periodicals; Computer programs -- Periodicals; 005.3
• DOI: 10.1002/spe.2959
• Languages: English
• ISSNs: 0038-0644

Abstract

Abstract: A significant aspect of designing new programming languages is to define their operational semantics. Working with a pen and paper version of such a semantics is notoriously difficult. For this reason, tools for computer aided semantics engineering were created. Many of these tools allow programmers to execute their language's operational semantics. An executable semantics makes it easier to verify whether the execution of a program leads to the desired result. When a program exhibits unexpected behavior, the programmer can consult the reduction graph to see what went wrong. Unfortunately, visualization of these graphs is currently not well‐supported by most tools. Consequently, the comprehension of errors remains challenging. In this article, we present GraphRedex an open‐source tool that empowers language designers to interactively explore their reduction graphs, offering three main benefits. First, a global exploration mode allows users to obtain a bird's‐eye overview of the reduction graph and learn its high level workings. Second, a local exploration mode lets the programmer closely interact with the individual reduction rules. Third, our query interface allows the programmer to filter out and highlight specific regions of the reduction graph. We evaluated our tool by carrying out a user study showing that participants comprehend programs on average twice as fast while being able to answer questions more accurately. Finally, we demonstrate how GraphRedex helps to understand the semantics of two published works. Exploration of the semantics with GraphRedex unveiled an issue in one of the implementations of these works, which the author confirmed.