Formal-Specification-to-Code Trace Links Recovery

The experiment data and the code used in our experiments to evaluate the performance of the proposed formal-specification-to-code trace links establishment method, and the other exsiting text-based trace links recovery methods, including Latent Semantic Indexing, Vector Space Model, Word2Vec embeddings, and LLM-based embeddings, are here. It originate from three projects. The first one is an open source VDM-SL specification of an AccountSys and its Java implementation. It comes from the book “Formal Software Development: From VDM to Java” written by Quentin Charatan and Aaron Kans. Both the VDM-SL formal specification and the Java implementation of the AccountSys were developed and provided by Prof. Aaron Kans from University of East London. It illustrates how to model bank accounts and transactions made on these as a series of deposits and withdrawals. Bank.java file implementing the GUI of the system in the source code is not used since it contains syntactical error and cannot build AST. The second project involves the SOFL specification and the Java implementation of an ATM system. The operations on current accounts of an ATM, such as deposit, withdraw, show balance, print out transaction records are specified by using SOFL formal language and implemented by using Java langauge. The third project involves an open source VDM-SL specification of a hotel system along with its C implementation. The specification describes a hotel management system where guests can check in, enter rooms, and manage cards associated with rooms and keys. The VDM-SL specification, created by Daniel Jackson and presented in his book “Software Abstractions: Logic, Language, and Analysis”.