| 正则表达式与有穷自动机等价性在Isabelle/HOL中的形式化 |
| |
| 引用本文： | 吴春寒,张兴元,贺汛.正则表达式与有穷自动机等价性在Isabelle/HOL中的形式化[J].解放军理工大学学报,2010,11(4):403-407. |
| |
| 作者姓名： | 吴春寒 张兴元 贺汛 |
| |
| 作者单位： | 解放军理工大学,指挥自动化学院,江苏,南京,210007 |
| |
| 基金项目： | 国家863计划资助项目 |
| |
| 摘 要： | 针对正则表达式和有穷自动机,在机器辅助定理证明系统Isabelle/HOL中进行了形式化描述。通过对语言、正则表达式、确定和不确定有穷自动机在Isabelle/HOL中建立模型,定义了它们之间的相互转换函数并证明了这些函数的正确性,从而验证了正则表达式和有穷自动机在描述能力上的等价性,即:在同一有限字母表下,对任意正则表达式,都存在一个有穷自动机,使得二者描述的语言相同;反之亦然。通过分析与证明,表明采用机器辅助定理证明系统,对计算理论传统核心领域之一的自动机理论进行分析和证明是可行的。
|
| 关 键 词： | 正则表达式 有穷自动机 形式化验证 |
Mechanizing equivalence of regular expression and FA in Isabelle/ HOL |
| |
| WU Chun-han,ZHANG Xing-yuan and HE Xun.Mechanizing equivalence of regular expression and FA in Isabelle/ HOL[J].Journal of PLA University of Science and Technology(Natural Science Edition),2010,11(4):403-407. |
| |
| Authors: | WU Chun-han ZHANG Xing-yuan and HE Xun |
| |
| Institution: | Institute of Command Automation,PLA Univ.of Sci.& Tech.,Nanjing 210007,China;Institute of Command Automation,PLA Univ.of Sci.& Tech.,Nanjing 210007,China;Institute of Command Automation,PLA Univ.of Sci.& Tech.,Nanjing 210007,China |
| |
| Abstract: | |
| |
| Keywords: | Isabelle/HOL |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《解放军理工大学学报》浏览原始摘要信息 |
| 点击此处可从《解放军理工大学学报》下载免费的PDF全文 |
|
