1

2 つの関数定義を検討してください

  test1 (x:nat) res:set of nat
    == { m | m:nat & m in set {0,...,x} };

  test2 (x:nat) res:set of nat
    == { m | m in set {0,...,x} & true };

Overture で test2(1000) を実行すると、1000 までの自然数のセットが得られます。test1(1000) を実行すると、255 までの自然数のセットが得られます。明示的な関数定義に明示的な型バインディングがあると複雑になることは理解していますが、この場合、黙って間違った答えを出すだけです。自然数の型束縛が定義に現れると、その範囲は 0..255 に制限されるようです。少なくとも、それは外部から起こっているようです。

言語マニュアルの第 8 章には、「型バインドは、型が静的に有限であると推定できる場合にのみ、VDM インタープリターによってのみ実行できることに注意してください。」と記載されています。型が静的に有限であると推定できる場合の規則はありますか?

4

2 に答える 2

1

ここで何が起こっているのかわかりません。Overture 2.3.0 (および 2.3.1 スナップショットと VDMJ) でこの仕様を試すと、test1 関数は常にすぐに次のように言って失敗します。

Error 4: Cannot get bind values for type nat

より大きな仕様の一部としてこのテストを実行していますか? マニュアルは正しいです。Overture は、"bool" のように型が有限であるか、または "set of bool" や "map P to Q" (P と Q が有限である) のように完全に有限型で構成されるものであると判断できない限り、型バインディングを実行できません。

基本的な有限型は bool とすべての quote 型です。これらの型は、"set of" などの型コンストラクターを使用してより複雑な型を構築するために使用できます。"seq of" を除くすべての型コンストラクターは、すべてのメンバー型が有限である限り、有限型を生成します。これには、[オプションの] 型、A*B のような製品型、A|B|C のような型共用体、およびレコード コンストラクターが含まれることに注意してください。

于 2016-02-15T09:40:58.370 に答える