Abstract: In order to guarantee the procedure accurate, it is necessary to examine whether it satisfies program＇s property before used. XYZ/AE is one sub-language of the temporal logical system XYZ. Describing program＇s property with XYZ/AE has superiority comparab

Key words: Program＇ s property, XYZ/AE, XYZ/EE