1

システムの仕様を B メソッドで書いています。一般的なセットのサブセットである次の変数があります。

  1. 最初の記法: a :={x,y,z,v} b :={x,y,z}

セット "b" に何かが存在する場合は常に、セット "a" にも存在するという規則を述べたいと思います。これは、上記の仕様を次のように記述するのに役立ちます。

  1. 2番目の表記: a :={v} b :={x,y,z}

2 番目の表記の説明: a :={v}、b :={x,y,z}、および規則から a :={x,y,z,v} をマシンに推論させたい。

最初の表記を避け、代わりに 2 番目の表記を書くようにルールを表現するにはどうすればよいでしょうか?

次のことを試しましたが、うまくいきませんでした

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

2 に答える 2

0

まず、述語!x.(x:b => x:a)は だけで簡単に表現できますb<:a。

あなたが何を表現したいのか正確にはわかりません:b常に初期化のサブセットであるa必要がありますか?

常にであれば、INVARIANTがその正しい場所になります。ASSERTIONSは似ていますが、他の不変条件による含意である必要があります。ただし、初期化で明示的に確認する必要があります。

私にとって不明確なもう1つの点は、「推測」の意味です。詳細を指定したくないだけですか？aset に 1 つ以上の要素を割り当てる初期化はb、次のようになります (との要素が含まれているaと仮定します)。bS

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 に答える