Xref: utzoo comp.lang.c:11506 comp.arch:5704
Path: utzoo!attcan!uunet!lll-winken!lll-tis!mordor!joyce!sri-unix!garth!smryan
From: smryan@garth.UUCP (Steven Ryan)
Newsgroups: comp.lang.c,comp.arch
Subject: Re: Self-modifying code
Message-ID: <1075@garth.UUCP>
Date: 25 Jul 88 19:52:41 GMT
References: <5262@june.cs.washington.edu> <260@thor.wright.EDU> <759@cernvax.UUCP> <472@m3.mfci.UUCP> <60782@sun.uucp> <473@m3.mfci.UUCP> <1988Jul23.221743.22169@utzoo.uucp> <477@m3.mfci.UUCP>
Reply-To: smryan@garth.UUCP (Steven Ryan)
Organization: INTERGRAPH (APD) -- Palo Alto, CA
Lines: 17

>If the machine allows a change to one variable (an array, say) to
>affect some other unrelated variable, then it is not conforming to
>the intent of my program.  In fact, it is not conforming to anything
>useful at all, since nobody would argue that it is useful programming
>practice to ever do such a thing on purpose (I hope?).

This particular example is done all the time in handling recursive data
structures.

>>Can it be done?  Well, in one sense the answer is clearly yes, because a
>>proof of program correctness has to include it, and we know that automating
>>such proofs is possible (although seldom practical at the moment).

Depends on whether all possible programs (including those of monkey
programmers) or just `practical' programs are considerred. Formal proofs
of all possible programs are impossible, flat out, no appeal. Formal proofs
of practical programs depend on how powerful practical has to be to remain
useful.