formal-methods

5熱度

1回答

我是一名（理論）計算機科學專業的學生，因此對編程語言語義的研究是我研究的主題之一（wikipedia）。我玩過很多CSS，對盒子定位規則有合理的理解。（如果您告訴我創建一個具有特定佈局的頁面，我經常會想到正確的方框和適用的CSS規則。）對CSS盒子定位規則有某種形式的語義會很酷，但在搜索了一段時間後，我無法找到任何有用的東西。我大部分只是簡單地結束於CSS規範，它被格式化爲具有僞算法的長

1熱度

3回答

正式方法 - 代數規範vs面向對象

我正處於一些研究的中間，一直未能找到很多文獻來幫助，我想比較兩種形式方法的平臺依賴關係;代數規範和麪向對象。他們將使用哪種語言？有沒有人有這方面的知識或可以指向正確的方向？謝謝

1熱度

1回答

把一門語言的語法（寫成ANTLR）轉化爲形式語言/數學符號

在我目前的項目中，我的老闆已經指派了一個將領域特定語言的語法（用ANTLR編寫）表達爲正式語言/符號的工作。例如，以下是語法的一小段代碼片段。 vocabSpec : 'resources' ':' resources_def ; // Resource definition resources_def : 'sensors' ':' (sensor_def)+ //

3熱度

1回答

合金4.2的語義變化對合金書的練習A.1.6的影響？

根據合金4.2的release notes，存在與整數有關的語義變化。這些變化似乎對合金書的練習A.1.6有影響。在本練習中，以下代碼作爲基礎給出（我在最後添加了「Int」以顯示我的問題）。當運行「顯示」謂詞時，可視化工具將顯示一個實例，但除了整數外，此實例還包含另外兩個原子「Univ0」和「Univ1」。 module exercises/spanning pred isTree(r: u

0熱度

1回答

如何顯示集合關係的「數量」？

請看看下面的 taking’ = taking ∪ {s? → m?} 正如你所看到的，taking是一個關係，其中s映射到m的名稱。上面的關係顯示了添加過程（聯合），我在這個關係中添加了一個新的maptlet。但是，我需要得到此關係中可用的s的編號。我怎麼才能得到它？下面是我做了什麼 #taking = numberOfStudents 但我不知道這件事。請幫助

2熱度

1回答

Z符號：2D陣列的表示

我是Z符號的完整初學者。我需要在Z中表示一個圖類型。我擁有的想法是使用一個關聯矩陣，以便我可以輕鬆地在節點和邊之間自由移動。唯一的問題是，我不知道如何指定Z中的關聯矩陣。我認爲我需要一個二維數組，但通過查看可用於Z表示法的參考資料，數組通常用起。是否有另一種方式來指定多維數組？在此先感謝。

2熱度

1回答

填充合金中的一組隨着時間的推移在一個完全連接的網絡

跟進從this question ... 我有一個完全連通圖，這是偉大的。我也加入了時間概念。我現在正在圍繞我的圖傳遞數據的概念而掙扎。我正在對一個系統進行建模，該系統的任務是確保每個節點都有一份已插入系統的數據副本。我已經掌握瞭如何做到這一點的程序，但是我正在努力將它翻譯成Alloy術語。一個典型的算法將是這個樣子： For i = 0 to TIME_STEPS: For eac

2熱度

1回答

在形式邏輯中證明正確性

我想知道是否有人能幫我回答這個問題。它來自之前的考試報告，我可以在知道準備好今年考試的答案的情況下做。這個問題似乎很簡單，我完全失去了，究竟是什麼要求？考慮代碼涉及整數變量的以下部分： if (i < j) { m = i; } else { m = j; } 通過規定適當的輸出條件，然後驗證正確性的代碼段的，證明執行之後，m是等於 i和j的最小值。我已經拿到了

0熱度

1回答

如何將if語句添加到模式的後置條件中？

我將簡化這個場景的事情（它在Perfect Developer中，它變得非常快速）。比方說，我的班級中有一個簡單的架構，名爲Succeed，它採用Course（這是一個以前定義的類）作爲參數。基本上，我想確保課程在我的課程set作爲前提條件，然後將其添加到我的後置條件中設置的我的coursesCompleted。這個簡單的模式的偉大工程，看起來像這樣： schema !Succeed(c:Cou

19熱度

1回答

SMT解算器的限制

傳統上，大多數使用計算邏輯的工作是命題性的，在這種情況下，您使用了SAT（布爾可滿足性）求解器或一階，在這種情況下，您使用了一階定理證明器。近年來，SMT（可滿足性模數理論）求解器取得了很大進展，基本上用算術等理論增強了命題邏輯。 SRI International的John Rushby甚至稱他們爲顛覆性技術。什麼是可以在一階邏輯中處理但仍不能由SMT處理的問題的最重要的實際例子？最特別的是