-
OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs
Authors:
Ján Perháč,
Samuel Novotný,
Sergej Chodarev,
Joachim Tilsted Kristensen,
Lars Tveito,
Oleks Shturmov,
Michael Kirkedal Thomsen
Abstract:
OnlineProver is an interactive proof assistant tailored for the educational setting. Its main features include a user-friendly interface for editing and checking proofs. The user interface provides feedback directly within the derivation, based on error messages from a proof-checking web service. A basic philosophy of the tool is that it should aid the student while still ensuring that the student…
▽ More
OnlineProver is an interactive proof assistant tailored for the educational setting. Its main features include a user-friendly interface for editing and checking proofs. The user interface provides feedback directly within the derivation, based on error messages from a proof-checking web service. A basic philosophy of the tool is that it should aid the student while still ensuring that the students construct the proofs as if they were working on paper.
We gathered feedback on the tool through a questionnaire, and we conducted an intervention to assess its effectiveness for students in a classroom setting, alongside an evaluation of technical aspects. The initial intervention showed that students were satisfied with using OnlineProver as part of their coursework, providing initial confirmation of the learning approach behind it. This gives clear directions for future developments, with the potential to find and evaluate how OnlineProver can improve the teaching of natural deduction.
△ Less
Submitted 9 May, 2025;
originally announced May 2025.
-
Local Software Buildability across Java Versions (Registered Report)
Authors:
Matúš Sulír,
Jaroslav Porubän,
Sergej Chodarev
Abstract:
Context: Downloading the source code of open-source Java projects and building them on a local computer using Maven, Gradle, or Ant is a common activity performed by researchers and practitioners. Multiple studies so far found that about 40-60% of such attempts fail. Our experience from the last years suggests that the proportion of failed builds rises continually even further. Objective: First, w…
▽ More
Context: Downloading the source code of open-source Java projects and building them on a local computer using Maven, Gradle, or Ant is a common activity performed by researchers and practitioners. Multiple studies so far found that about 40-60% of such attempts fail. Our experience from the last years suggests that the proportion of failed builds rises continually even further. Objective: First, we would like to empirically confirm our hypothesis that with increasing Java versions, the percentage of build-failing projects tends to grow. Next, nine supplementary research questions are proposed, related mainly to the proportions of failing projects, universal version compatibility, failures under specific JDK versions, success rates of build tools, wrappers, and failure reasons. Method: We will sample 2,500 random pure-Java projects having a build configuration file and fulfilling basic quality criteria from GitHub. We will try to automatically build every project in containers with Java versions 6 to 23 installed. Success or failure will be determined by exit codes, and standard output and error streams will be saved. A majority of the analysis will be performed automatically using reproducible scripts.
△ Less
Submitted 21 August, 2024;
originally announced August 2024.
-
Outside the Sandbox: A Study of Input/Output Methods in Java
Authors:
Matúš Sulír,
Sergej Chodarev,
Milan Nosáľ
Abstract:
Programming languages often demarcate the internal sandbox, consisting of entities such as objects and variables, from the outside world, e.g., files or network. Although communication with the external world poses fundamental challenges for live programming, reversible debugging, testing, and program analysis in general, studies about this phenomenon are rare. In this paper, we present a prelimin…
▽ More
Programming languages often demarcate the internal sandbox, consisting of entities such as objects and variables, from the outside world, e.g., files or network. Although communication with the external world poses fundamental challenges for live programming, reversible debugging, testing, and program analysis in general, studies about this phenomenon are rare. In this paper, we present a preliminary empirical study about the prevalence of input/output (I/O) method usage in Java. We manually categorized 1435 native methods in a Java Standard Edition distribution into non-I/O and I/O-related methods, which were further classified into areas such as desktop or file-related ones. According to the static analysis of a call graph for 798 projects, about 57% of methods potentially call I/O natives. The results of dynamic analysis on 16 benchmarks showed that 21% of the executed methods directly or indirectly called an I/O native. We conclude that neglecting I/O is not a viable option for tool designers and suggest the integration of I/O-related metadata with source code to facilitate their querying.
△ Less
Submitted 20 June, 2023;
originally announced June 2023.
-
Automating Test Case Identification in Java Open Source Projects on GitHub
Authors:
Matej Madeja,
Jaroslav Porubän,
Michaela Bačíková,
Matúš Sulír,
Ján Juhár,
Sergej Chodarev,
Filip Gurbáľ
Abstract:
Software testing is one of the very important Quality Assurance (QA) components. A lot of researchers deal with the testing process in terms of tester motivation and how tests should or should not be written. However, it is not known from the recommendations how the tests are written in real projects. In this paper, the following was investigated: (i) the denotation of the word "test" in different…
▽ More
Software testing is one of the very important Quality Assurance (QA) components. A lot of researchers deal with the testing process in terms of tester motivation and how tests should or should not be written. However, it is not known from the recommendations how the tests are written in real projects. In this paper, the following was investigated: (i) the denotation of the word "test" in different natural languages; (ii) whether the number of occurrences of the word "test" correlates with the number of test cases; and (iii) what testing frameworks are mostly used. The analysis was performed on 38 GitHub open source repositories thoroughly selected from the set of 4.3M GitHub projects. We analyzed 20,340 test cases in 803 classes manually and 170k classes using an automated approach. The results show that: (i) there exists a weak correlation (r = 0.655) between the number of occurrences of the word "test" and the number of test cases in a class; (ii) the proposed algorithm using static file analysis correctly detected 97% of test cases; (iii) 15% of the analyzed classes used main() function whose represent regular Java programs that test the production code without using any third-party framework. The identification of such tests is very complex due to implementation diversity. The results may be leveraged to more quickly identify and locate test cases in a repository, to understand practices in customized testing solutions, and to mine tests to improve program comprehension in the future.
△ Less
Submitted 30 July, 2021; v1 submitted 23 February, 2021;
originally announced February 2021.
-
Visual augmentation of source code editors: A systematic mapping study
Authors:
Matúš Sulír,
Michaela Bačíková,
Sergej Chodarev,
Jaroslav Porubän
Abstract:
Source code written in textual programming languages is typically edited in integrated development environments or specialized code editors. These tools often display various visual items, such as icons, color highlights or more advanced graphical overlays directly in the main editable source code view. We call such visualizations source code editor augmentation.
In this paper, we present a firs…
▽ More
Source code written in textual programming languages is typically edited in integrated development environments or specialized code editors. These tools often display various visual items, such as icons, color highlights or more advanced graphical overlays directly in the main editable source code view. We call such visualizations source code editor augmentation.
In this paper, we present a first systematic mapping study of source code editor augmentation tools and approaches. We manually reviewed the metadata of 5,553 articles published during the last twenty years in two phases -- keyword search and references search. The result is a list of 103 relevant articles and a taxonomy of source code editor augmentation tools with seven dimensions, which we used to categorize the resulting list of the surveyed articles.
We also provide the definition of the term source code editor augmentation, along with a brief overview of historical development and augmentations available in current industrial IDEs.
△ Less
Submitted 10 November, 2018; v1 submitted 5 April, 2018;
originally announced April 2018.
