formal-methods

1熱度

1回答

我定義2種幾乎相同的語言（foo和bar）： theory SimpTr imports Main begin type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype foo_exp = FooBConst bool | FooIConst int |

-1熱度

1回答

公理語義 - 如何計算最弱的前提

這裏是例子： x = y + 1; y = y - 2; {y < 3} 什麼是這個例子中的最弱前置條件？我想也許y < 3是一個答案。如果不是，你能詳細告訴我爲什麼嗎？

0熱度

1回答

VDM中的遞歸函數

如何定義遞歸函數來查找VDM中小於輸入數的兩個最大冪？的功能如下：最大：N - >ñ 所有到目前爲止，我所得到的是：最大（N）= 如果n = 1然後0 否則如果n = 2，則1 否則......最大的（...）

2熱度

1回答

有沒有辦法找到在合金中運行「沒有實例找到」的原因？

我用合金寫過模型。但是，對於運行謂詞來查找實例的某些條件失敗，它說沒有找到實例。我嘗試增加約16個實例的綁定，但它沒有找到任何實例。有沒有什麼辦法可以調試這個，這樣我就可以看到哪些事實失敗，導致Alloy無法找到實例？謝謝！

1熱度

1回答

細化B型規範

的考慮我在B型規範如下： - flower <: FLOWER age <: AGE owner <: OWNER Type <: flower * age Buyer : owner <-> flower 是否有可能對我來說，隨後創建一個細化： - flower <: FLOWER age <: AGE owner <: OWNER Type : Owner <-> flowe

1熱度

1回答

不能讓類型類在精益中工作

我無法理解如何觸發精益類型類的使用。這裏是一個小例子，企圖： section the_section structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a) definition P A := exists (a : A), forall x, x = a parameter A : T

2熱度

1回答

我可以說狀態空間是一些系統行爲的正式規範嗎？

給定一個系統及其完整的狀態空間，我可以說那個狀態空間是該系統行爲的正式規範嗎？

0熱度

2回答

你如何證明遞歸列表長度的終止？

假設我們有一個清單： List = nil | Cons(car cdr:List). 請注意，我說的是修改列表！而一個簡單的遞歸長度功能： recursive Length(List l) = match l with | nil => 0 | Cons(car cdr) => 1 + Length cdr end. 當然，它結束只有當列表爲非圓形： induct

2熱度

1回答

驗證程序的等價性

優化編譯器的最終目的是在程序空間中搜索等價於原始程序但速度更快的程序。這已經在實踐中用於非常小的基本塊：https://en.wikipedia.org/wiki/Superoptimization 聽起來很難的部分是搜索空間的指數性質，但實際上它不是;最難的部分是，假設你找到了你想找的東西，你如何證明這個新的，更快的程序與原始程序真的是相同的？上次我研究過它，在某些情況下證明程序的某些屬性已經

1熱度

1回答

Zed的規範：促進和應用操作一個以上的架構

我有一個Array模式，它跟蹤的Data模式序列。使用促銷，我可以促進Increment操作使用Array。 ArrayIncrement只在Array內增加一個數據。我該如何使它在\ran data中每增加Data？