Path: utzoo!attcan!uunet!ogicse!ucsd!ucbvax!agate!alfa.berkeley.edu!bks
From: bks@alfa.berkeley.edu (Brad Sherman)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <1990Mar16.210324.398@agate.berkeley.edu>
Date: 16 Mar 90 21:03:24 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <1423@oravax.UUCP>
Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44)
Reply-To: bks@alfa.berkeley.edu (Brad Sherman)
Organization: University of California, Berkeley
Lines: 44

In article <1423@oravax.UUCP> ian@oravax.odyssey.UUCP (Ian Sutherland) writes:
>In article <2480006@hpcuhc.HP.COM> runyan@hpcuhc.HP.COM (Mark Runyan) writes:
>-As an alternative, someone could post a non-trivial program and ask the
>-program provers to prove it either correct or incorrect...
>I like this idea.  Any takers?
>Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Well this is trivial, but I think many of us would like to see some
examples of program proofs so let's start out small. Is this correct or
not?

/* ---------------------------------------------------------------------
 *      RXUTOS
 *      RadiX Unsigned TO String.
 *      Converts an unsigned integer into a string of digits in any
 *      base (radix) in the range {2, ..., 35}.  Digits needed in the range
 *      {10, ..., 35} are represented by the characters {A, B, ..., Z}.
 *
 *      This function returns a pointer to a static buffer which is
 *      overwritten on each call. On error (radix out of range), a NULL
 *      pointer is returned.
 *
 *      Author: Bradley K. Sherman (bks@alfa.berkeley.edu)
 *      Copyright (C), The Regents of the University of California, 1990
 */
char *
rxutos( n, radix )
unsigned int   n;
unsigned int   radix;
{
        static char	buf[ ( 8 * sizeof(unsigned int) ) + 1 ];
        char		*s = ( 8 * sizeof(unsigned int) ) + buf;   
 
        if ( radix < 2  ||  radix > 35 ) 
           return( NULL );
 
        *s = '\0'; 
        do {
                *--s = "0123456789ABCDEFGHIJKLMOPQRSTUVWXYZ"[n % radix];
        } while ( (n /= radix) > 0 );
 
        return( s );
}
/* --------------------- End of function rxutos() ---------------------  */