[cap-talk] C vs. Safety

[Toby Murray]

On Thu, 2008-08-07 at 14:10 -0700, Tony Bartoletti wrote:
> At 01:29 PM 8/7/2008, Valerio Bellizzomi wrote:
> Mathematicians would love to know if there exists an (extended) 
> integer N > 1 for which the following procedure fails to exit:
> 
>    k = N;
>    while( k > 1 )
>    {
>          if( k%2 ) // k is ODD
>                  k = (3*k+1)/2;
>          else    k = k/2;
>    }
>    exit();
> 
> ... or a proof that no such N exists (the process ALWAYS exits) ...
> 

I don't know what an "extended" integer is... perhaps this is the reason
for the following, however. 

Surely (assuming arbitrary precision integer arithmetic) termination
here can be proved as follows.

Unwind the loop once to arrive at

K=N
if (k>1){
   if (k%s){
      k = (3*k+1)/2;
   }else{
      k = k/2;
   }
}

// invariant: k is even or k == 1
// variant: k - 1
while (k>1){
   if (k%s){
      k = (3*k+1)/2;
   }else{
      k = k/2;
   }
}

We can use weakest-precondition predicate transformers to show that 
{N>1} P {k is even or k == 1}
for P as the if-block.

Given this, as the comments suggest, the second loop can be shown to
terminate using the given invariant and variant, i.e. for Q as the
program-fragment that is the while-loop, we can show

{k is even or k == 1} Q {true}

The invariant (which is true before the loop executes) is maintained by
the loop and the variant decreases each time through until it reaches 0
at which point the loop terminates.

This analysis, if correct, shows that the program, say S, satisfies
{N>1} S {true}
i.e. S terminates for all N>1.
  
What am I missing? 

Cheers

Toby