問題タブ [dafny]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
dafny - 証人 null の試行: 操作の結果がサブセット型の制約に違反する可能性があります
セット S の 2 項関係を表すクラスを作成しました。このクラスには、2 つのフィールドがあります。そのセット S と、S から引き出された値のペアの 2 番目のセットです。単一値であること (つまり、「isFunction()」述語で定義されている関数であること)。クラス定義の後、いくつかのサブセット タイプを定義しようとします。1つは、実際には「関数」でもあるこれらの関係のサブタイプを定義することを目的としています。動作していません。結果のエラー コードを解読するのは少し難しいです。Valid() および isFunction() 述語は「reads this;」を宣言していることに注意してください。私がどこを見なければならないかについてのアイデアはありますか？Dafny はサブセット タイプが生息していることを認識できないということでしょうか。だと納得させる方法はありますか？
[Dafny VSCode] 証人 null の試行: 操作の結果が「binRelOnS」のサブセット型制約に違反する可能性があります
dafny - Dafny の型制約: 二項関係型の「表示」の実装
Dafny でポリモーフィック バイナリ リレーション タイプ (クラス) を定義しました。
実際の宣言は次のとおりです。
新しい型制約を追加したいと思います。型 S と T は "表示" 操作 (文字列を返す) を実装する必要があります。
私が Dafny リファレンス マニュアルを読んだところ、Dafny がサポートする組み込みの型制約は == と明らかに !new のみであり、特定のトレイトなど、その型のサポートを要求する方法はありません。
おそらく私は間違っており、リファレンス マニュアルよりも最近の更新でそのような機能が提供されています。私は運がいいですか？そうでない場合、おそらく回避策はありますか？