Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!ucbvax!ulysses!kpv
From: kpv@ulysses.att.com (Phong Vo[drew])
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <14633@ulysses.att.com>
Date: 21 Apr 91 17:24:59 GMT
References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu> <12318@dog.ee.lbl.gov>
Organization: AT&T Bell Laboratories, Murray Hill
Lines: 25

In article <12318@dog.ee.lbl.gov>, torek@elf.ee.lbl.gov (Chris Torek) writes:
> >If it's proven mathematically, it *will* work.
> (To argue David Gudeman's side:)  *What* will work?
> If your proof is correct, you have shown that your program P1 in
> language L1 is mathematically equivalent to some other program P2 in
> some other language L2.  There are no guarantees that the assumptions
> made in the process (that compiler C1 for language P1 `works', that
> program P2 has the desired effect in all circumstances, and so on) are
> all correct.
> 
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.