Abstract

Abstract
Formal verification has become increasingly crucial in ensuring the accurate and secure functioning of modern software systems. Given a specification of the desired behaviour, i.e. a contract, a program is considered to be correct when all possible executions guarantee the specification. Should the software fail to behave as expected, then a bug is present. Most existing research assumes that the bug is present in the implementation, but it is also often the case that the specified expectations are incorrect, meaning that it is the specification that must be repaired. Research and tools for providing alternative specifications that fix details missing during contract definition, considering that the implementation is correct, are scarce. This paper presents a preliminary tool, focused on Dafny programs, for automatic specification repair in contract programming. Given a Dafny program that fails to verify, the tool suggests corrections that repair the specification. Our approach is inspired by a technique previously proposed for another contract programming language and relies on Daikon for dynamic invariant inference. Although the tool is focused on Dafny, it makes use of specification repair techniques that are generally applicable to programming languages that support contracts. Such a tool can be valuable in various scenarios, such as when programmers have a reference implementation and need to analyse their contract options, or in educational contexts, where it can provide students with hints to correct their contracts. The results of the evaluation show that the approach is feasible in Dafny and that the overall process has reasonable performance but that there are stages of the process that need further improvements.

Abstract

Abstract
Background: Many programming environments include automated feedback in the form of hints to help novices learn autonomously. Some experimental studies investigated the impact of automated hints in the immediate performance and learning retention in that context. Automated feedback is also becoming a popular research topic in the context of formal specification languages, but so far no experimental studies have been conducted to assess its impact while learning such languages. Objective: We aim to investigate the impact of different types of automated hints while learning a formal specification language, not only in terms of immediate performance and learning retention, but also in the emotional response of the students. Method: We conducted a simple one-factor randomised experiment in 2 sessions involving 85 BSc students majoring in CSE. In the 1st session students were divided in 1 control group and 3 experimental groups, each receiving a different type of hint while learning to specify simple requirements with the Alloy formal specification language. To assess the impact of hints on learning retention, in the 2nd session, 1 week later, students had no hints while formalising requirements. Before and after each session the students answered a standard self-reporting emotional survey to assess their emotional response to the experiment. Results: Of the 3 types of hints considered, only those pointing to the precise location of an error had a positive impact on the immediate performance and none had significant impact in learning retention. Hint availability also causes a significant impact on the emotional response, but no significant emotional impact exists once hints are no longer available (i.e. no deprivation effects were detected). Conclusion: Although none of the evaluated hints had an impact on learning retention, learning a formal specification language with an environment that provides hints with precise error locations seems to contribute to a better overall experience without apparent drawbacks. Further studies are needed to investigate if other kind of feedback, namely hints combined with some sort of self-explanation prompts, can have a positive impact in learning retention. © 2024 Copyright held by the owner/author(s).