Path: utzoo!utgpu!news-server.csri.toronto.edu!clyde.concordia.ca!uunet!mcsun!hp4nl!fwi.uva.nl!kim!freek
From: freek@fwi.uva.nl (Freek Wiedijk)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <534@fwi.uva.nl>
Date: 17 Mar 90 00:30:43 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <1423@oravax.UUCP> <1990Mar16.210324.398@agate.berkeley.edu>
Sender: news@fwi.uva.nl
Reply-To: freek@fwi.uva.nl (Freek Wiedijk)
Organization: Faculteit Wiskunde & Informatica, Universiteit van Amsterdam
Lines: 29

In article <1990Mar16.210324.398@agate.berkeley.edu> bks@alfa.berkeley.edu (Brad Sherman) writes:
>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?

No:
>                *--s = "0123456789ABCDEFGHIJKLMOPQRSTUVWXYZ"[n % radix];
                                               ^^
You forgot the N!  (I'm sure, I'll be the Nth to reply with this :-)

Other criticisms: You never defined NULL, and your program is _much_
too long, it should have been: :-) :-)

/*(c)*/char*rxutos(n,r)unsigned n,r;{static char b[8*sizeof(unsigned)
+1];char*s=8*sizeof(unsigned)+b;if(r<2||r>35)return(0);*s=0;do{*--s=
"0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"[n%r];}while((n/=r));return(s);}

Also: what's wrong with radix 36?

--
Freek "the Pistol Major" Wiedijk                  Path: uunet!fwi.uva.nl!freek
#P:+/ = #+/P?*+/ = i<<*+/P?*+/ = +/i<<**P?*+/ = +/(i<<*P?)*+/ = +/+/(i<<*P?)**