Abstract: Code function description extraction is the basic premise of functional integration. To address the problem of common low accuracy rate of extraction of code function, the mechanism of extracting code function description based on formal semantic of Clight was proposed, and it was realized by algorithm of Clight code function description. This mechanism was strictly based on Clight natural semantics inference rules, ignoring the details of code execution in the middle, only concerned with the memory states before and after implementation. And as a functional description of the code feature description, it improved the accuracy of functional extraction and the success rate of the key area in software development.

Key words: functional integration, formal semantics, Clight, natural semantic, code function, description extraction

摘要： 软件代码的功能提取是功能集成的最基本前提，但软件功能提取普遍存在正确率低的问题。为此，提出基于Clight形式语义的代码功能描述提取机制，并用Clight代码功能描述算法实现。该机制严格基于Clight自然语义推理规则，忽略代码执行的中间细节，只关注执行前后的存储状态，并以此作为代码的功能描述，提高了功能提取的正确率和关键领域软件开发的成功率。

关键词: 功能集成, 形式语义, Clight, 自然语义, 代码功能, 描述提取