【摘要】 本文前半部分致力于建立一种(无穷)程序逻辑的基础。作为这种形式的逻辑的应用,后半部分证明了一个强终结定理,即任何具强终结性质的程序都可等价于一个无循环程序。更多还原

【Abstract】 An extended dynamic logic is developed by using a special (infinitary) descriptive language as the building basis. Then a theorem that each strong terminating program is equivalent to a loop-free program is proved.更多还原