セット S の 2 項関係を表すクラスを作成しました。このクラスには、2 つのフィールドがあります。そのセット S と、S から引き出された値のペアの 2 番目のセットです。単一値であること (つまり、「isFunction()」述語で定義されている関数であること)。クラス定義の後、いくつかのサブセット タイプを定義しようとします。1つは、実際には「関数」でもあるこれらの関係のサブタイプを定義することを目的としています。動作していません。結果のエラー コードを解読するのは少し難しいです。Valid() および isFunction() 述語は「reads this;」を宣言していることに注意してください。私がどこを見なければならないかについてのアイデアはありますか？Dafny はサブセット タイプが生息していることを認識できないということでしょうか。だと納得させる方法はありますか？
type func<T> = f: binRelOnS<T> | f.Valid() && f.isFunction()
[Dafny VSCode] 証人 null の試行: 操作の結果が「binRelOnS」のサブセット型制約に違反する可能性があります