Выражение правил в B-методе

Question

Я пишу некоторые спецификации системы в B-метод. У меня есть следующие переменные, которые являются подмножествами общего набора:

1. Первая запись: a:={x,y,z,v} b:={x,y,z}

Я хочу сформулировать правило, что всякий раз, когда что-то существует в наборе "b", оно также существует в наборе "a", которое помогает писать вышеуказанные спецификации следующим образом:

2. вторая запись: a:={v} b:={x,y,z}

Объяснение второй нотации: я хочу, чтобы машина выводила, что a: = {x, y, z, v} из a:={v}, b:={x,y,z} и правила.

Как я могу выразить правило, чтобы избежать первой нотации и вместо этого написать вторую нотацию?

Я попробовал следующее, но это не сработало

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

Answer 1

Прежде всего, предикат !x.(x:b => x:a) может быть легче выразить просто b<:a,

Мне не ясно, что именно вы хотите выразить b всегда быть подмножеством a или только в инициализации?

Если всегда, то INVARIANT будет правильным местом для этого. ASSERTIONS похожи, но должны быть следствием других инвариантов. Но тогда вы должны явно убедиться, что в вашей инициализации.

Другой момент, который мне неясен, это то, что вы подразумеваете под "сделать вывод". Вы просто не хотите уточнить детали? Инициализация, где вы назначаете a установить с одним элементом более 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} ))

Answer 2

Во-первых, и прежде всего, машина B ничего не выводит сама по себе. Он предоставляет язык, на котором пользователь может выражать свойства, и механизм, который генерирует проверочные обязательства, которые должны быть успешно обработаны проверяющим (автоматически или с помощью человека), чтобы гарантировать, что свойства сохраняются.

В вашем примере, если вы хотите выразить, что каждый элемент множества bb всегда элемент множества aaтогда как заметил даниэльп, просто напиши

bb <: aa

Далее, если вы хотите написать, что aa относится к элементу, который не находится в bbтогда вы можете выразить это как

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

или как

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

Если вы хотите выразить это конкретное значение vv в aa но не в 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