Optimizing Isabelle2Cpp for Safe and Efficient C++ Codes Generation
DongChen Jiang, YongKang Mao, Bo XuABSTRACT
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.