編譯細節和可達性算法F＃

我應該如何分析圖形各部分的可達性（稱爲規則）：如果驗證某個布爾條件，則可以到達節點。每個節點只知道它的前任，有不同類型的節點，並不是所有的節點都有一個需要檢驗的條件。該規則放置在一個文件中。編譯細節和可達性算法F＃

我做了規則的解析，我選擇了（通過使用區別聯合）並根據執行流程對節點進行了排序。現在，我應該做一種靜態分析來通知用戶，對於指定的情況，有些節點是不可訪問的。圖形有多個入口點，但只有一個出口點。

教授告訴我翻譯F＃中的布爾條件並通過編譯檢查它。但我注意到，F＃編譯器不給我，即使我寫了下面的代碼，一個警告：

let tryCondition cond = 
if cond then 
    if not cond then "Not reachable" 
    else "Reachable" 
else "bye"

或

let tryConditionTwo num = 
match num with 
| x as t when x > 0 -> match t with 
         | y when y < 0 -> "Not reachable" 
         | _ -> "Reachable" 
| _ -> "bye"

是否有更好的解決方案並沒有太多複雜的實施中F＃來解決這個問題？或者在編譯器中有一個選項可以讓我獲得有關不可達代碼的信息？

編輯：這是一個圖表的例子，我必須檢查各個分支的可達性。「IN」塊用於從數據庫加載列，而「選擇」塊用於選擇所有且僅滿足給定條件的行。我應該靜靜地檢查這些條件是相互矛盾的。

An example of rule graph

來源

2011-06-15 marcx87

還有就是要解決這個問題沒有簡單的方法。如果您能夠編寫一個始終有效的靜態分析工具，那麼您也可以解決Halting problem，這是可能的（可能）。

我不認爲F＃編譯器目前有任何複雜的可達性分析。如果你想只爲布爾條件和整數（如你的例子中）執行這個檢查，那麼你可以解析F＃表達式，將它轉換成一些邏輯公式，然後使用SMT solver來檢查是否有任何值的條件將保持。

要解析的源代碼，您可以使用open-source F#釋放，或者您可以使用F＃報價（如果你只是想上明確標記的表達運行的工具）。使用後者更容易啓動。
有關SMT求解器的更多信息，可以查看來自Microsoft Research的Z3 project。你也可以自己實現一個簡單版本的工具 - 只要布爾條件（沒有數字），你可以看看SAT solving algorithms。

來源

2011-06-15 10:15:29

感謝您的回覆。現在我記錄下來，你會知道這是否是我需要的。我添加了一些筆記和一張我希望能夠說明的圖片。 – marcx87 2011-06-15 12:46:18

編譯細節和可達性算法F＃

回答

相關問題