event-b

    5熱度

    2回答

    event-b：是否有可能通過一個表達式中的lambda生成從...到...素數的序列？

    我想知道是否可以用event-b中的一個lambda表達式生成素數序列。這是我迄今爲止： @axm1 primeSet = {x∣ x ∈ 1‥100 ∧ ¬(∃y·y < x ∧ y > 1 ∧ x mod y = 0)} ∧ finite(primeSet) @axm2 primeSeq ∈ 1‥card(primeSet) >->> primeSet @axm3 ∀a,b,c,d·a↦b
    lambda sequence primes formal-methods event-b 2014-02-07

    1熱度

    1回答

    事件B證明義務

    我在事件B中有問題來履行證明義務。在我的工作中，我想正式確定內存保護要求的規範，以檢查它們之間的一致性。爲了做到這一點，我使用了Event-B上下文來形式化系統結構，並使用Event-B Machine來描述需求。 Invariant和Event都描述了每個需求。事件-B將檢查每對要求以找出不一致。 但是，它不能證明兩者的要求是一致的： 1： 「從讀訪問不可信到DATA_SECTION其他OS_A
    operating-system event-b formalize 2017-07-18

    0熱度

    1回答

    事件-B羅丹平臺，建模子集關係

    我是事件-B的初學者，我試圖模擬一臺機器，其中設置的PERSONNE包括集合客戶端，其中包括設置RESIDENT ...我' VE搜查羅丹的文檔，但我沒有發現任何東西...... 這裏是上下文 context contexteHumain sets PERSONNE CLIENT RESIDENT axioms @axm1; finite(PERSONNE) @axm2
    event-b 2015-04-04

    1熱度

    2回答

    獲取變量的首要/下一個狀態

    給定一些條件，我想檢查變量下一個狀態是否適用於某個命題。我無法創造出羅丹接受的東西。 我的確切情況是下面的不變。我想確保鎖定開啓時變量door不會改變。變量door或者是Open或Closed inv4: PrimaryLock = On ⇒ door :∣ door' = door 如果PrimaryLock是On這意味着門狀態不會改變，不管未來會觸發什麼事件。 這是可能的使用事件b或我需要
    event-b 2015-12-11

    1熱度

    1回答

    活動B總功能

    我有一個問題如下： 小學班包含了一些兒童和各種書籍。寫一個跟蹤孩子讀過的書的模型。它應該保持兒童與書籍之間的關係。還應該處理以下事件： 記錄：增加的事實，給孩子閱讀給定書 newbook：輸出一書中說，鑑於孩子沒有讀過 books_query：輸出的書籍給孩子已經閱讀 這裏的數字是我的模型至今 CONTEXT booksContext SETS STUDENTS B
    event-b 2014-03-19
最新問題