問題タブ [vdm-sl]

これは比較的簡単なはずだと思いますが、誰かがこれに答える方法を知っているかどうか疑問に思っていました:

自然数列の最小値を返す再帰関数 seq-min : N+ -> N を定義します。

・・・のようなことを考えていました。

助けてくれてありがとう！

これがSOの領域内にあるかどうかはわかりませんが、

VDM-SL を使用して、ℕ の単一の有限サブセットを記述する「最良の」方法を探し回っています。旅行中に、人々がこれを伝える方法をいくつか見つけましたが、どれが最も受け入れられているのだろうか.

私は当初、F(ℕ) でよいと考えていましたが、これは単一のサブセットではなく、ℕ の有限サブセットのセットであると考えています。

「S を有限にしよう: S ⊂ ℕ?」と言うだけで十分でしょうか?

それともそういう表記はありますか？

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

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

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

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

VDM-SL Toolbox で作業しようとしていますが、チュートリアルが見つかりません。誰かがチュートリアルを持っている場合は、共有してください。ありがとうございました