# IRC log for #isabelle, 2011-10-13

All times shown according to UTC.

Time Nick Message
15:28 hakzsam joined #isabelle
15:29 hakzsam hi all
15:29 hakzsam I need some help for proving some algorithms with the Hoare logic
15:34 monochrom I haven't used isabelle for a long time. but do you have pretty good preconditions and postconditions that you think are right?
15:35 hakzsam actually, I never used isabelle
15:35 hakzsam but I'm trying to solve some algorithms...
15:36 hakzsam I want to prove this following code http://pastebin.com/5kEfyUG4
15:36 hakzsam I already have a precondition, a postcondition and a loop invariant
15:37 hakzsam monochrom, could you give me some help ?
15:39 monochrom I get "unknown paste ID"
15:39 hakzsam mmh.. sorry
15:39 hakzsam the paste is probably outdated
15:39 hakzsam http://pastebin.com/eGkTY3eR
15:41 monochrom but what are the preconditions and postconditions?
15:43 hakzsam http://pastebin.com/HC8ywbhv
15:43 hakzsam {I} is the loop invariant I found
15:44 hakzsam now, I want to prove the loop invariant
15:45 monochrom your invariant won't work
15:45 hakzsam mmh.. what is the problem ?
15:46 monochrom in Q, "ok=true" won't work either. the point of the program is that ok is false when the array a is not a palindrome
15:47 hakzsam arf, {Q} is wrong too
15:47 monochrom "a[i]=a[j]" is simply not an invariant.
15:47 hakzsam indeed, ok is false when the array a is not a palindrome
15:47 hakzsam mmh...
15:48 hakzsam btw, I'm a newcomer
15:48 hakzsam could you give me some hints in order to solve that problem ?
15:50 hakzsam do you agree with this logic representation { j = n-1, forall i ∈ 0..j, a(i) = a(j-i) ∧ ok = true } for a palindrome ?
15:50 monochrom of course not
15:51 hakzsam arf, so, what is the *correct* representation ?
15:51 monochrom try not to reuse the names i and j
15:52 hakzsam could you explain why, please ? I'm not sure to understand what you mean
15:54 monochrom alright, I erred, your formula is almost correct, but it has an off-by-1 error
15:55 monochrom also the postcondition is way more than saying "a is a palindrome".
15:55 monochrom I am not sure what you want right now, whether the full postcondition or just the part that says "a is a palindrome"
15:58 hakzsam yes, the full postcondition, please
15:59 monochrom what symbol do you use for "if and only if"?
16:01 hakzsam mmh.. I think I never used "if and only if" in logic, so you can use your own representation
16:01 monochrom ok = (forall x ∈ 0..n-1, a(x) = a(n-1-x))
16:01 monochrom (so I also erred: you did not have an off-by-1 error)
16:02 hakzsam ok :)
16:03 hakzsam <monochrom> ok = (forall x ∈ 0..n-1, a(x) = a(n-1-x))
16:03 hakzsam that's the full postcondition or just "a is a palindrome" ?
16:03 monochrom full postcondition
16:04 monochrom I wouldn't mention "ok" just for the palindrome part, obviously.
16:04 hakzsam ok
16:05 hakzsam and why the loop invariant is wrong ?
16:05 monochrom because a(i) can be different from a(j)
16:06 monochrom you even have the code to test a(i)=a(j) every iteration.
16:07 hakzsam that's true, indeed
16:08 hakzsam I'm sorry, but I don't understand why did you remove "∧ ok = true" in the postcondition :S
16:09 monochrom because ok can be false at the end
16:09 hakzsam ah yes, I understand
16:09 hakzsam obviously
16:09 hakzsam so, now I must to find the correct loop invariant because a(i) = (j) is wrong
16:10 hakzsam *must find
16:11 monochrom at the beginning of an iteration, you already know that part of the array has already been checked and looks like a palindrome
16:13 monochrom for example you already know a(0)=a(n-1), a(1)=a(n-2), a(2)=a(n-3). this is the state when i=3 and ok is still true and you are just before "if a(i)=a(j) then"
16:14 monochrom you also know that i+j=n-1 always
16:14 hakzsam got it !
16:14 hakzsam so, the invariant is i+j = n-1 ?
16:14 monochrom you also know i<=j. so basically P is part of the invariant
16:15 monochrom i+j=n-1 is part of the invariant. there is more. i+j=n-1 alone won't get you the postcondition
16:15 hakzsam mmh... P is the precondition, right ?
16:15 hakzsam but I found that P = {true}, that's wrong too ?
16:15 monochrom P is your i<=j ∧ ok=true
16:16 monochrom sorry, B.
16:16 hakzsam ok
16:21 monochrom i+j=n-1 ∧ ok = (forall x ∈ 0..i-1, a(x) = a(n-1-x))
16:22 monochrom the invariant shouldn't include the while-loop's guard (i<=j ∧ ok)
16:23 hakzsam ok, I think I understood my mistake, thanks
16:24 monochrom the invariant should look like the postcondition with some change in parameters (e.g., change n-1 to i-1), and whatever extra help information (e.g., i+j=n-1)
16:26 monochrom you may throw in i>=0 if you find it useful
16:26 hakzsam ok
16:31 monochrom my invariant is still wrong. it would be right if the code always incremeneted i and decremented j, i.e., "if a[i]=a[j] then ... else ok:=false i:=i+1 j:=j-1 endif".
16:31 monochrom so now I have an off-by-1 error too
16:33 monochrom the correct invariant to match this code is a bit complicated. i+j=n-1 ∧ (ok ⇒ (forall x ∈ 0..i-1, a(x) = a(n-1-x))) ∧ (¬ok ⇒ a(i)≠a(n-1-i))
16:36 monochrom if ok is true, I know that previous iterations have checked the array up to and including a(i-1) for palindromeness, but haven't checked a(i). but if ok is false, that's because the previous iteration has found a(i)≠a(j) which is a(i)≠(n-1-i), and the previous iteration hasn't incremented i since.
16:37 monochrom so it's ugly, sometimes it hasn't checked a(i) yet, sometimes it has already.
17:08 hakzsam thanks for your help monochrom, I have all informations in my mind in order to solve my problem now :)