A structured temporal logic language: XYZ/SE 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 is 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.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- He, Pei; Yao, Yuehua; Ye, Jixiang: A study of an integrated proof strategy (1999)
- Xie, Hongliang; Gong, Jie; Tang, C.S.: A structured temporal logic language: XYZ/SE (1991)