Background Isabelle2Cpp is a general framework that enables automatic C++ codes generation from Isabelle/HOL specifications. However, the generated codes may lead to data safety problems in secondary development, and there is still room for efficiency improvement of the generated codes. Objectives The purpose of this paper is to improve the execution efficiency of the generated codes by Isabelle2Cpp while ensuring data safety. Methods To achieve that, deep copy is generated in the type codes for data safety; shallow copy, reference, and move are used to eliminate redundant value copies; memoization is employed to avoid repetitive computations, and target type selection is provided for users to improve the performance of C++ codes in the rule‐based conversion. Results The correctness of the conversion is demonstrated, and experiments across different aspects are conducted to evaluate the effectiveness of the optimized framework.
No takes yet. Share an insight, caveat, or question.
Jiang et al. (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: