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

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

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