1

我正在用 B 方法编写系统的一些规范。我有以下变量，它们是一般集合的子集：

  1. 第一个符号：a :={x,y,z,v} b :={x,y,z}

我想声明一个规则，只要集合“b”中存在某些东西，它也存在于集合“a”中，这有助于将上述规范编写如下：

  1. 第二种表示法：a :={v} b :={x,y,z}

第二个符号的解释：我希望机器从 a :={v}、b :={x,y,z} 和规则中推断出 a :={x,y,z,v}。

我怎样才能表达规则，所以我避免第一个符号，而是写第二个符号？

我尝试了以下但没有奏效

INITIALISATION 
    a :={v} & 
    b :={x,y,z}
ASSERTIONS
    !x.(x:b => x:a)
4

2 回答 2

0

首先，最重要的是，B 机器本身不会推断出任何东西。它提供了一种用户可以表达属性的语言和一种生成证明义务的机制，证明义务必须由证明者（自动或在人工协助下）成功处理以保证属性成立。

在您的示例中，如果您想表达 set 的每个元素bb始终是 set 的一个元素aa，那么正如 danielp 所观察到的那样，只需编写

bb <: aa

接下来，如果你想写出aa拥有一个不在 中的元素bb，那么你可以将其表示为

aa /= bb & not(aa = {})

或作为

#(elem).(elem : S & elem : bb & not(elem : aa))

如果您更想表达特定值vv在 inaa而不是 in bb，则以下适用

vv : bb & not(vv : aa)

这些表达式可以在 B 机器的多个位置使用，具体取决于您是要断言参数、常量还是变量的属性。

例如，假设您有一台具有两个变量va和的机器vb，其中两者都是给定集合 的元素集s1，并且您希望它们以这样的方式初始化，即 的每个元素vb也是 的元素va，并且存在那个元素va不在vb. 首先观察这意味着vb是 的严格子集va。

INITIALISATION
  ANY inia, inib WHERE
    inia <: s1 & inib <: s2 & inib <<: inia
  THEN
    va := inia || vb := inib
  END
于 2017-06-09T09:30:46.887 回答
0

首先，谓词!x.(x:b => x:a)可以更容易地用 来表示b<:a。

我不清楚您到底想表达什么：应该b始终是初始化的子集a还是仅在初始化中？

如果总是这样，那INVARIANT将是正确的位置。ASSERTIONS是相似的，但应该是其他不变量的暗示。但是，您必须在初始化时明确确保这一点。

我不清楚的另一点是您所说的“推断”是什么意思。您只是不想指定详细信息吗？您a为 set 分配一个多于一个元素的初始化b可能如下所示（假设a并b包含 的元素S）：

INITIALISATION
  ANY v,s
  WHERE
      v:S
    & s<:S
  THEN
      a := s\/{v}
   || b := s
  END

（免责声明：我还没有实际测试过。）

如果a应该总是大于b，你可以添加类似v/:s. 您的描述并没有明确说明您想要实现的目标。

另一种方法是使用“成为这样的替代”（但在我看来，它的可读性较差）：

INITIALISATION
     a,b :( a:S & b:S &
            b={x,y,z} & 
            #x.( x:S & a=b\/{x} ))
于 2016-08-11T15:21:21.200 回答