V2EX = way to explore
V2EX 是一个关于分享和探索的地方
Sign Up Now
For Existing Member  Sign In
syncher
V2EX  ›  问与答

怎样找"循环不变式"?

  •  
  •   syncher · Mar 7, 2017 · 3143 views
    This topic created in 3348 days ago, the information mentioned may be changed or developed.

    算法导论中讲到一个概念就是循环不变式,知乎上有人提出"如何正确理解循环不变式?"(参见:https://www.zhihu.com/question/26700198) ,我现在大致理解了一些,大概就是每次执行循环总有一些特性保持不变,但是对于一个具体的案例还是不会找循环不变式,如求一个数组的最大值:

    max = A[1] for i = 1 to A.length if A[i] > max max = A[i]

    请问该如何找该算法中的循环不变式?

    5 replies    2017-03-08 12:09:41 +08:00
    yangff
        1
    yangff  
       Mar 7, 2017
    max 是 a[1..i]的最大值
    yangff
        2
    yangff  
       Mar 7, 2017   ❤️ 1
    是这样的,现在我要证明`max = A[1] for i = 1 to A.length if A[i] > max max = A[i]`这个程序能给出 A[]这个数组的最大值,我们没办法一条一条地考察这个程序,因为循环的存在,他可能被执行任意多次

    怎么做,一个直观的想法就是,我要有一个特性能得到最后的正确性,并且这个特性总成立。

    在这里就是

    “对于一个有限长度的 n (循环终止时), max 是 A[1..n]中最大的”

    那么对于这段程序,用归纳法,显然 n=1 的正确性

    若假设 n=k 正确,当 n=k+1 时,我们首先有 max 是 a[1..k]的最大值,又由` A[i] > max max = A[i] `, 使之成为 A[1..k+1]的最大值

    于是就可归纳得到对于任意长度(终止的 n ) max ,也就是 max 是 A[1..n]中最大的得证

    从而证明了循环的正确性
    syncher
        3
    syncher  
    OP
       Mar 8, 2017
    感谢楼主,好像懂了,比如:
    for i = 1 to n sum += i 这个循环体只有一个表达是 sum += i; 那么循环中保持不变的特性就是 sum 总是 1,2,...,i 的和,这个特性就是循环不变式,是吗?
    syncher
        4
    syncher  
    OP
       Mar 8, 2017
    @yangff 感谢楼主,好像懂了,比如:
    for i = 1 to n sum += i 这个循环体只有一个表达是 sum += i; 那么循环中保持不变的特性就是 sum 总是 1,2,...,i 的和,这个特性就是循环不变式,是吗?
    yangff
        5
    yangff  
       Mar 8, 2017
    @syncher
    About   ·   Help   ·   Advertise   ·   Blog   ·   API   ·   FAQ   ·   Solana   ·   3962 Online   Highest 6679   ·     Select Language
    创意工作者们的社区
    World is powered by solitude
    VERSION: 3.9.8.5 · 31ms · UTC 10:23 · PVG 18:23 · LAX 03:23 · JFK 06:23
    ♥ Do have faith in what you're doing.