Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!apple!motcsd!hpda!hpcupt1!hpisod2!decot
From: decot@hpisod2.HP.COM (Dave Decot)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <16520018@hpisod2.HP.COM>
Date: 19 Mar 90 22:02:09 GMT
References: <52044@microsoft.UUCP>
Organization: Hewlett Packard, Cupertino
Lines: 76

> This really isn't the way it's done.  The idea is to develop the
> program and its proof simultaneously.  The generation of invariants
> and assertions is more difficult (at least now, since there is not
> as much cultural experience) than writing the code.
> 
> Eric Hughes

Righto.  For discussion purposes, here's the specification version
of the radix conversion code (somebody else will have to come up with
the invariants and assertions).

Dave
-----------

/*  This a version of the original program with its initial
    comments converted into a C-like specification language.
    The meaning of the language constructs are intended to be
    obvious.  The use of the keyword "return" in this language
    refers to the return value of the function.
*/

/* The original specification doesn't mention radix, so the function
   could have been implemented more easily by returning "6" always.  :-)
   However, assuming that the return value should be a numeral
   representing the value of n in the indicated radix...
*/

/* Import precompiled specifications of various functions; assume that
   they are specified as in ANSI C.
*/

extern spec int strlen();
extern spec char *strchr();
extern spec long strtoul();

#define digits "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"

spec char *rxutos(n, radix)
register unsigned int n, radix;
{
    if (radix >= 2 && radix <= 36)
    {
	forall int i (i >= 0 && i <= strlen(return))
	{
	    define char *p (strchr(return[i], digits));
	    guarantee p != 0 && p - return < radix;
	}

        guarantee strtoul(return, (char **)0, radix) == n;
	guarantee strlen(return) < 8*sizeof(unsigned int) + 1;
    }
    else
	guarantee return == 0;
}

/* for comparison, here's the posted implementation */

char *rxutos(n, radix)
register unsigned int n;
register unsigned int radix;
{
        static char buf[ (8 * sizeof(unsigned int)) + 1 ];
        char *s = (8 * sizeof(unsigned int)) + buf;   
 
        if ( radix < 2  ||  radix > 36 ) 
           return( 0 );

        *s = '\0';
        do {
		--s;
                *s = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"[n % radix];
		n /= radix;
        } while ( n > 0 );
 
        return( s );
}