程序綜合技術(shù)的研究與實現(xiàn).pdf

1、該文所討論的是實現(xiàn)軟件自動化的一個重要方法---程序綜合的技術(shù)及其實現(xiàn).該技術(shù)以程序變換和演繹推理為基礎(chǔ),其基本思想是:根據(jù)程序的目的寫出滿足需求的但不含任何算法提示的程序規(guī)范,根據(jù)一些法則和變換規(guī)則反復(fù)變換程序規(guī)范,直到推導(dǎo)出滿意的遞歸程序.其主要特點是:對程序的規(guī)范不進行正確性證明,推導(dǎo)的過程就是證明的過程.該文分別對保結(jié)構(gòu)和變結(jié)構(gòu)兩種程序的綜合進行了闡述.在保結(jié)構(gòu)程序綜合過程中引進了條件引入,遞歸調(diào)用形成,遞歸的推廣,輔助過程的形

2、成等法則,提出了在程序綜合過程中通過改變設(shè)計決策可以綜合出相同問題的不同算法族.在變結(jié)構(gòu)程序綜合中,為了消除程序中的副作用引進了與Z.Manna不同且效率更高的回溯技術(shù).最后,該文介紹了一個數(shù)組型程序綜合系統(tǒng)APSS,其中提出了條件變換規(guī)則組概念,說明了通過選擇不同的條件規(guī)則組來綜合出滿足不同需求的程序.此外,為了更詳細,清楚地介紹上述程序綜合技術(shù),該文還列舉了一系列復(fù)雜程序不同,涉及數(shù)值計算,樹結(jié)構(gòu)問題,表的處理,數(shù)組計算等程序?qū)嵗?