Question

{Q} = {n>0}
C1 = i := 1;
C2 = c := 1;
C3 = p := 0;
{P} = {i<=n, p = fib(i-1), c = fib(i)}

My lack of understanding towards the rule of consequence in hoare logic is blocking me from find the solution which i hope someone can shed some light on how can i approach this with minimal abstraction of the process.

{R} = {i<=n,p=fib(i-1),c=fib(i)[i\1]} i:= 1;{i<=n, p = fib(i-1), c = fib(i)}

{R} = {1<=n,p=fib(0),c=fib(1)}

{R} = {1<=n,p=0,c=1}

{R1} = {1<=n,p=0,c=1[c\1]}c:=1;{1<=n,p=0,c=1}

{R1} = {1<=n, p=0, true }

{R2} = {1<=n,p=0[p\0]}p:=0;{1<=n,p=0}

{R2} = {1<=n, true}{1<=n,p=0}

{R2} = {1<=n -> 0>x} :( i can't arrive at exactly n>0

*edit

From my observation the key problem is regardless of sequence i would always arrive at 1<= n as not equivalent to n>0, i am not sure how i can legally perform P->P’ P’ C Q’ Q’->Q to prove {P}C{Q}

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top