問題タブ [vdm++]

私は過去 2 週間、大学のコースワークに取り組んできましたが、その 90% をかなり完了しました。Overture を開くことにしましたが、すべてのプロジェクトが破損しているようです :((((((

http://gyazo.com/8e25549bbca700a22399e736a88a1996

これから回復する方法について誰か提案/アイデアがあれば、大いに感謝します。「比較 -> ローカル履歴」を試しましたが、うまくいきませんでした。今は少し動揺しています:[

Overture で VDM 数学構文を使用することは可能ですか、それとも ASCII 構文に制限されていますか?

または、LaTeX を生成するときに、出力に数学構文を使用できますか?

LaTeXはほとんど使ったことがありません。出力「.tex」を取得し、TeXファイルで「forall」を「\ forall」に置き換えてからPDFを再生成しようとしましたが、PDFに「\ forall」が挿入されただけです。同じ結果で '$\forall$' に疲れました。

ところで、VDMとOvertureを組み合わせることで、仕様を作成するための素晴らしい環境が整います。

Overture であるモジュールから別のモジュールをインポートすると、すべてが非常に簡単になります。ただし、別のプロジェクトからモジュールをインポートする方法がわかりません。私がすることは：

• プロジェクト P1 を作成
• P1 にモジュール A を作成する
• プロジェクト P2 を作成
• P1 を P2 の参照として指定
• P2 にモジュール B を作成する
• モジュールBでインポートA

モジュール B では、システムは「A のようなモジュールはありません」というエラーにフラグを立てます。

Modelio と Overture を一緒に使用して、UML と VDM でプログラムをモデル化する方法を学びたいです。UML モデルの作成、XMI (uml 拡張) へのエクスポート、および Overture へのインポートに関する手順全体が正常に完了しました。

しかし、それを Modelio にエクスポートしようとすると、「失敗しました: ファイルの内容が有効なモデルとして認識されません」というメッセージが表示されます。Overture のチュートリアルでは、前後にインポート/エクスポートすることが可能であると述べています。ただし、現時点では機能が壊れているようです。

私は何か間違ったことをしているかもしれません。エクスポートされた XMI ファイルを Modelio が理解できるように、Overture を特定の方法で設定する必要があるかもしれません。解決策をオンラインで検索することはすべて失敗しました。Overture から Modelio に正常にエクスポート/インポートするにはどうすればよいですか?

Modelio 3.4.1 と Overture 2.3.0 を使用しています。

ありがとうございました。

拡張された明示的な関数でいくつかの興味深い動作が見られます。

陰関数を定義する

対応する明示的な関数 (事後条件は計算可能であるため)

isLeap2 は期待される値を返します。次に、拡張陰関数を定義します

これは、100 の倍数であるが 400 ではない引数が指定されている場合を除いて、期待どおりに機能します。結果は次のとおりです。

次に、これを入力しているときに、次のことを考えました。

そして結果は予想通り。このコンテキストでの「=」と「<=>」の違いは何ですか? VDM-10 言語マニュアル (2014 年 11 月発行) のセクション 3.1.1 には、「ブール値を扱う場合、意味的に <=> と = は同等である」と記載されています。操作性に違いはありますか？

コール スタックの深さが最大 ​​1000 の入力に対して機能する再帰関数がありますが、より大きな入力に対しては失敗します。関数を末尾再帰に変換したところ、約 1350 に到達できました。

制限とは何ですか? また、その制限を増やす方法はありますか?

私は純粋な関数で作業しており、操作を使用する必要がないようにしたいと考えています。問題をステップの構成に分割するソリューションがあります。各ステップのスタックの深さは小さくなりますが、その唯一の目的は問題を回避することであり、より複雑であるため、かなり不自然です。

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

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

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

私は、アプリケーション全体を反復的に構築することに焦点を当てた本の演習を行ってきました。4 つのクラスを作成した後、4 番目のクラスのテストである 5 番目のクラスを作成しています。ただし、Overture は「名前 'BinBuilder()' は範囲外です」というエラーを報告しています。BinBuilder は、私が作成に成功した最後のクラスです。今回は自分が何をしているのか理解できません。問題を引き起こしているクラスは BinBuilder だけではなく、他の 2 つのクラスも同様です。何が悪いのかわからないので、ここに全体へのリンクを含めます。ありがとうございました。

編集: Overture からエクスポートされた zip ファイルをリンクしており、エラーを示すスクリーン キャプチャが含まれています。

実数を自然数に丸めたいとしたら、VDM++ でこれを行うにはどうすればよいでしょうか? MATH ライブラリには、これを行う関数がないようです。

ありがとう、リカルド