Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!think.com!mintaka!bloom-beacon!eru!kth.se!sunic!mcsun!hp4nl!charon!guido
From: guido@cwi.nl (Guido van Rossum)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <3380@charon.cwi.nl>
Date: 21 Apr 91 20:38:00 GMT
References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu> <12318@dog.ee.lbl.gov> <14633@ulysses.att.com>
Sender: news@cwi.nl
Lines: 28

kpv@ulysses.att.com (Phong Vo[drew]) writes:
>Just to make this concrete, the following example is mathematically correct
>given all the usual definitions of the C operators. It is incorrect because
>it is not portable.

>	int strlen(register char *str)
>	{
>		register char	*sp = str-1;
>		while(*++sp)
>			;
>		return(sp-str);
>	}

>The problem is in the assignment 'sp = str-1'. On some machine, this will
>cause a core dump when the while() loop is executed first time even though
>the ++ should make sp valid.

The program makes *another* assumption which makes it non-portable: it
assumes that the string size is less than the maximum integer, which
may be as small as 32767.

It is hard enough to prove that a given C program is correct if one
knows all the environment parameters (integer size, etc.).  How about
proving that a C program is correct under all legal combinations of
environment parameters?

--Guido van Rossum, CWI, Amsterdam <guido@cwi.nl>
"You're so *digital*, girl!"