問題タブ [loop-invariant]

特定の時間単位で2つの日付間の時間を計算することになっている非常に単純な関数がありgetPartialPeriod(January 1, February 15, months)ます1.5。

私はそれを証明する方法に本当に苦労しています - それが最も難しい部分だと思うので、私はループから始めました. 多数の Hoare トリプルとループ不変条件を定義しましたが、それらはすべて役に立たないことがわかりました。これで得られるすべての助けに感謝します。

関数の擬似コード:

PS 少しばかげた実装のように見えることは無視してください - それは重要ではありません。

ループ不変条件について読んだことがありますが、少し混乱しています。
このコードがあるとしましょう。不変条件は何でしょうか? A+B =X のようなもの？

ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):

M[x <- N] は、M 内のすべての x を N に置き換えます。

さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。

編集：参照要求を避けるために言い換えました。

私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。

計算理論コースで反復プログラム/関数の正しさを証明するという概念を理解するのに苦労しています。より具体的には、ループ不変条件を考え出す方法がわかりません。関数が複数のループ不変条件を持つことができることは理解していますが、事後条件を証明するのに役立つ不変条件を見つける方法については、完全な謎です。私は現在、いくつかの宿題に取り組んでおり、次の関数のループ不変式を見つける方法がわかりません。

今のところ、関数がどのように機能するかは理解していますが、前に述べたように、この関数が a^b を返すことを示すのに役立つ適切なループ不変条件を見つけようとすると、非常に途方に暮れます。

割り当ての場合、二分探索を使用して整数の平方根を見つけるメソッドを作成する必要があります。それが平方数でない場合は、s*s <= 数値となるような整数 s を返す必要があります (したがって、15 の場合は3) を返します。私がこれまでに持っているコードは

そして、これは平方数に対して正しい数を返しますが、他の整数に対しては無限ループに陥ります。問題が while 条件にあることはわかっていますが、数字が大きくなるにつれて平方数間のギャップが大きくなるため、何を入れればよいかわかりません (したがって、ギャップが以下でなければならないということは言えません)しきい値)。演習は不変条件に関するものであり、それが役立つ場合です (したがって、このように設定されている理由)。ありがとうございました。

このコードの不変条件が何であるかを理解する必要があります。複数の不変条件が存在する可能性があると思いますが、トピックをよく理解していません。また、見つけたオンライン リソースもまだ役に立ちません。二分探索用に作成したコードは次のとおりです。

このコードは、バイナリ検索を使用して整数の平方根を見つけますが、平方数でない場合は、整数より小さい最も近い平方数の平方根を返す必要があります。

コードは機能しますが、不変式として何を配置するか、および返される正しい値がどのように示されるかを実際に理解するだけです。手がかり/説明は素晴らしいでしょう、ありがとう。

整数の数字を逆にする次のコードがあります。

私の教授は、このコードを書くことを私たちに課し、ループ不変条件とループ条件も書くように言われました。ここでループ条件を理解していますが、不変条件について何を見ればよいかわかりません。while ループの開始時と終了時に真になるのは何らかの条件であることに気付きましたが、反復ごとに、ここで何が起こるかわかりません。ヒントをいただければ幸いです。