1

私は Eiffel で割り当てを行っていますが、ensure 句の実装に問題があります。変数または関数を含めるために必要な特別な構文はありますか?

これは、「put」関数の現時点での私のコードです

    put(key: K; value: V)
    require

            key /= void
    local
        tmp:ITEM[K,V]
    do

        create tmp.make(key, value)
        list.put_front (tmp)
        count := count + 1
    ensure

    count = old count + 1 and list.has(key, value)
    end

これは「has」関数のコードです

    has(key:K; val:V):BOOLEAN
require
    key /= void
local

    flag: INTEGER
    do

    flag := 0
    from
        list.start
    until
        list.exhausted
    loop
        if list.item.getkey = key then
            if list.item.getvalue = val then
                flag := 1
            end
        end
        list.forth
    end
    if flag = 1 then
        Result := true
    else
        Result := false
    end
    ensure
        --???   
end

割り当ては、リンクされたリストを介してマップ広告を実装することです。'put' 関数は、項目 (キー、値) をリストに挿入します。「has」関数は、リストに (キー値) ペアが含まれているかどうかをチェックします。

どんな助けでも大歓迎です。

4

1 に答える 1

1

それはただかもしれません

Result = across list as c some (c.item.key = key and c.item.value = value) end

ただし、コードには他にもいくつかのコメントがあります。

  1. プロパティが使用されている場所がわかりませんkey /= Void。なので必須ではないようです。
  2. のコードがputタイプ の要素を挿入することを考えるとITEM、 の事後条件も代わりに をput使用する必要があります。だから私はそれがその前にないだけであるべきだと思う.across list ... endlist.has (key, value)has (key, value)list.
  3. 補助変数を使用する意味がわかりませんflag。予約変数Resultは問題なく機能します。
  4. Eiffel のすべての変数はデフォルト値で初期化されるため、ルーチンの開始時に0to flag(または簡略化されたバージョンではfalseto ) を割り当てる必要はありません。Result
  5. 通常、Eiffel では専用のゲッターを用意する必要がないため、通常、コードlist.item.getkeyはlist.item.key.
  6. list.finish必要な要素が見つかったときに、カーソルをリストの最後の項目に移動するを呼び出すことで、先制的にループを終了できます。その後list.forth、ループ終了条件が満たされ、ループが終了します。
于 2013-05-26T15:21:35.340 に答える