從程序驗證到程序合成技术頭條網

2020-02-21 05:57:00 慕測科技

1 引用

Srivastava S , Gulwani S , Foster J S . From program verification to program synthesis[J]. ACM SIGPLAN Notices, 2010, 45(1):313.

2 摘要

自動程序合成在比可執行代碼更高級別上指定程序，可以使得編程和系統設計更加簡潔。而本文介紹了一種用於命令式程序合成的新技術，稱之為證明理論合成。這裡用戶提供輸入輸出功能說明，編程語言中原子操作的描述以及合成程序的循環結構，允許的堆棧空間和某些操作用法的綁定說明。如果存在滿足輸入輸出規範以及資源限制的程序，該技術則進行相應的程序合成。

該技術的獨到之處在於將程序合成轉換成程序驗證，這使得我們可以將現有的程序驗證工具和技術引入到程序合成中。我們的合成算法通過未知語句、衛、歸納不變式和排名函數來生成相應的程序。該合成算法然後生成與未知數相關的約束，並強制執行以下三種約束要求：部分正確性、循環終以及格式正確的條件。同時我們形式化這些對於程序驗證工具必須滿足以進行約束求解的規範，然後使用現有的工具作為我們的合成器。

我們通過在三個不同的領域中合成相關程序來證明所提出方法的可行性：算術，排序和動態規劃。使用我們先前在 VS 項目中內置的驗證工具，我們可以為複雜的算術算法合成程序，包括 Strassen 的矩陣乘法和 Bresenham 的線圖、集中分類算法和動態規劃算法。對於這些程序，合成時間的中值時間為 14 秒，合成時間與驗證時間的比率在 1 倍至 92 倍之間（中值為 7），這也表明了該技術在後續應用的潛力。

3 引言

自動化程序合成儘管有望大大減少編程任務負擔，但由於難以實現而很少受到研究人員關注。它減輕了與編程底層細節相關的繁瑣和錯誤，可以幫助進行自動調試，並且通常使人類程序員可以自由地處理系統的高層設計。同時，合成可以發現程序員難以構建的新的重要程序。

在本文中，我們提出了一種程序合成方法，該方法採用通過構造的程序設計哲學，並展示瞭如何使其自動化。程序驗證工具通常以歸納不變式的形式合成程序證明，以實現部分正確性，並對排名函數進行終止。通過將程序衛和語句編碼為需要發現的邏輯事實，我們將合成問題編碼為驗證問題，這使得我們可以使用某些驗證工具進行合成。驗證工具推斷出不變式和排名函數，並推斷出程序語句，從而實現自動化程序合成。我們將我們的方法稱為“證明理論合成”，因為證明是與程序是一起合成的

我們將合成任務定義為對輸出程序的要求：功能要求，對程序表達式和衛形式的要求以及對所用資源的要求。我們的合成算法的關鍵在於如何將合成任務減少到三組約束。第一組是確保程序中循環的部分正確性的安全條件。第二組是程序保護和語句的格式正確的條件，以使驗證工具的輸出與命令語言中的有效衛和語句相對應。第三組是確保程序終止的進度條件。據我們所知，我們的方法是第一種自動程序合成及其證明的方法，而先前的方法要麼使用給定的證明來提取程序，要麼沒有嘗試生成證明。

為了進一步我們的方法，接下來我們將展示如何合成相應的程序，儘管有些程序的要求很容易指定，但實際的程序卻相當複雜。

4 技術介紹

下面將詳細介紹合成技術的各個步驟，首先需要生成合成條件，這些條件是對語句，衛，循環不變式和排序函數的未知數的約束。然後我們注意到它們與驗證條件類似，並且可以使用驗證工具來進行求解。

4.1 合成概念介紹

本節將詳細介紹使用理論證明方法進行程序合成的相關要求以及用戶如何指定程序的空間。

合成支架：

我們使用一個支架來描述合成問題，其形式為

它的三個組成部分如下：

合成任務：

4.2 合成條件生成

（2）流程圖擴展

我們為流程圖模板中的每一個非循環片段和循環註釋合成代碼片段，形式上，其流程圖模板如下：

（3）編碼部分正確性：安全狀態

（4）編碼有性控制：格式正確的條件

接下來，我們構造約束以確保語句的格式正確，在之前的開發中，我們將選擇語句中的每條路徑視為獨立。在任何可執行程序中，控制將始終流經該語句的至少一個分支/轉換，並且每個轉換將包含格式正確的賦值語句。我們首先需要描述一個直接對此進行編碼的約束，然後討論如何確保轉換防護結構良好。

（5）編碼過程：排名函數

到目前為止，我們的編碼只針對安全條件，這些安全條件本身只能確保部分正確，而不能保證終止。接下來，我們需要添加進度約束以確保合成程序終止。

（6）整個合成條件

4.3 合成條件求解

圖 1 合成算法

5 本文主要貢獻

首先我們（1）提出了一種將合成任務指定為三元組的新穎方法，之後（2）將程序合成視為廣義的程序驗證，並正式定義了約束條件，也稱為合成條件，可以使用現有的驗證工具進行求解，同時（3）提出了程序驗證工具必須滿足的要求，以此進行程序語句的合成，最後（4）我們使用驗證工具構建了合成器，並在算術，排序和動態編程三個領域進行了合成評估。