计算机应用 ›› 2012, Vol. 32 ›› Issue (08): 2333-2337.DOI: 10.3724/SP.J.1087.2012.02333

• 典型应用 • 上一篇    下一篇

基于Clight形式语义的代码功能描述提取

王涛,陈敏翼,齐军   

  1. 华南师范大学 计算机学院,广州 510631
  • 收稿日期:2012-01-03 修回日期:2012-03-21 发布日期:2012-08-28 出版日期:2012-08-01
  • 通讯作者: 陈敏翼
  • 作者简介:王涛(1975-),男,广西合浦人,副教授,博士,主要研究方向:软件工程、形式化方法、信息系统安全;
    陈敏翼(1986-),男,广东潮州人,硕士,主要研究方向:软件工程、形式化方法;
    齐军(1987-),男,河南息县人,硕士,主要研究方向:软件工程、形式化方法。

Functional description extraction of code based on formal semantics of Clight

WANG Tao,CHEN Min-yi,QI Jun   

  1. School of Computer Science, South China Normal University, Guangzhou Guangdong 510631, China
  • Received:2012-01-03 Revised:2012-03-21 Online:2012-08-28 Published:2012-08-01
  • Contact: CHEN Min-yi

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

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

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

中图分类号: