摘要: 本文提出了一种抽象数学机——正则自动机（简称RA）作为程序流程的数学模型。为了描述RA的语义特性,文中把自动机理论中的正则语言与数理逻辑的模型论语言结合起来,建立了一种一阶谓词的动态逻辑语言（?）_R。文中表明,一些现有的程序逻辑公理系统,例如,著名的Hoare公理系统可以作为（?）_R的可证定理推导出来。论文的第一部分介绍了RA的基本概念,二讨论RA的语义学特性,三讨论了RA模型在程序分析与综合中的应用,四讨论了RA模型在递归一循环变换中的应用。