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 = n1, forall i ∈ 0..j, a(i) = a(ji) ∧ 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 offby1 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..n1, a(x) = a(n1x)) 
16:01 
monochrom 
(so I also erred: you did not have an offby1 error) 
16:02 
hakzsam 
ok :) 
16:03 
hakzsam 
<monochrom> ok = (forall x ∈ 0..n1, a(x) = a(n1x)) 
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(n1), a(1)=a(n2), a(2)=a(n3). 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=n1 always 
16:14 
hakzsam 
got it ! 
16:14 
hakzsam 
so, the invariant is i+j = n1 ? 
16:14 
monochrom 
you also know i<=j. so basically P is part of the invariant 
16:15 
monochrom 
i+j=n1 is part of the invariant. there is more. i+j=n1 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=n1 ∧ ok = (forall x ∈ 0..i1, a(x) = a(n1x)) 
16:22 
monochrom 
the invariant shouldn't include the whileloop'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 n1 to i1), and whatever extra help information (e.g., i+j=n1) 
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:=j1 endif". 
16:31 
monochrom 
so now I have an offby1 error too 
16:33 
monochrom 
the correct invariant to match this code is a bit complicated. i+j=n1 ∧ (ok ⇒ (forall x ∈ 0..i1, a(x) = a(n1x))) ∧ (¬ok ⇒ a(i)≠a(n1i)) 
16:36 
monochrom 
if ok is true, I know that previous iterations have checked the array up to and including a(i1) 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)≠(n1i), 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 :) 