問題タブ [dafny]

functionint のシーケンスを取り、ペアのシーケンスを返すdafny を作成するにはどうすればよいですか? 例: 入力 = [1,2]、出力 = [ペア(1,1)、ペア(1,2)]

私はから始めました

うまくいかないようです。

ダフニーを通過させるために、以下に何を追加する必要があるのだろうか？

検索、削除、および挿入メソッドを使用する検索および置換メソッドをコーディングしています。while ループ内でこれら 3 つのメソッドを呼び出していますが、どの前提条件を使用すればよいかわかりません。

完全なコード:

更新しました

特定のクラスとそれぞれのメソッドを使用して以下に説明する、いくつかのダフニーの問​​題を解決する際の問題。他に何か必要な場合は、教えてください。事前に感謝します。また、rise4fun のこのすべてのコードでリンクが更新されます。

オンライズ4ファン

文字の配列に重複が含まれているかどうかを判断する述語をdafnyで作成しようとしています。最終的には次のように何かをテストする必要があります。要素が 2 つ未満の場合は無視してください

ただし、次のテストを実行すると、アサーションに失敗します。なぜこうなった？

文字列にシーザー暗号を適用するプログラムを検証しようとしています。元の文字列を返す必要があります

次のように、文字列の値を更新する最良の方法は何ですか?

次の公理が与えられます。

N1==ADafnyを使用してそれを証明したいと思います。

次の Dafny プログラムを試しました。

しかし、ダフニーはそれを証明できません。N1==A与えられた公理から抜け出す方法はありますか?