1

VDM-SL で暗黙的な関数定義を使用して仕様を作成してきましたが、非常にうまく機能しています。ここで、明示的な関数定義を使用して仕様のプロトタイプを作成したいと考えています (この段階では操作はありません)。

私が見ることができる 1 つの方法は、暗黙的な仕様で定義された関数を模倣する新しいモジュールを作成することですが、それらに明示的な定義を与えることです。

これができると確信していますが、それが理想的であるとは思えません。暗黙の仕様と明示的な仕様の間にリンクはありませんが、一方は他方の改良版です。

暗黙的な関数定義から明示的な関数定義に移行するための推奨される方法はありますか? 長期的には、これを正式に調査したいと思っていますが、最初の例では、暗黙的な関数仕様を実装して、仕様の動作を実証したいと考えています。

4

1 に答える 1

1

仕様を改良するための正式なプロセスがありますが、特に現在それをサポートするツールがないため、非常に骨の折れる作業です。

暗黙的な関数型シグネチャと事前/事後条件を保持する場合、実装がすべての入力に対して正しいと仮定すると、明示的なバージョンは洗練されたものであることが「確実」になります (これは、組み合わせテストが役立つ場合です)。「暗黙の」スタイルで書かれた関数に実装 (本体) を与えることもできることに注意してください。

f(x:nat) r:nat
== x + 1        -- This line added to the implicit spec!
pre x > 10
post r < 100
于 2016-02-09T09:46:33.427 に答える