A Structured Temporal Logic Language:XYZ/SE  

作　　者：谢洪亮 龚洁 唐稚松 

机构地区：[1]Institute of Software,Academia Sinica,Beoing 100080

出　　处：《Journal of Computer Science & Technology》1991年第1期1-10,共10页计算机科学技术学报（英文版）

摘　　要：In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general compositional verification method in the XYZ system concerning the sequential case.In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general compositional verification method in the XYZ system concerning the sequential case.

关 键 词：A Structured Temporal Logic Language FTL 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]