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
最新问题