Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site wdl1.UUCP
Path: utzoo!dciem!nrcaero!pesnta!amd!fortune!wdl1!jbn
From: jbn@wdl1.UUCP
Newsgroups: net.lang
Subject: Re: Nil dereferencing protection
Message-ID: <257@wdl1.UUCP>
Date: Mon, 4-Feb-85 16:26:52 EST
Article-I.D.: wdl1.257
Posted: Mon Feb  4 16:26:52 1985
Date-Received: Thu, 7-Feb-85 07:29:50 EST
Sender: notes@wdl1.UUCP
Organization: Ford Aerospace, Western Development Laboratories
Lines: 11
Nf-ID: #R:harvard:-33800:wdl1:8600004:000:523
Nf-From: wdl1!jbn    Feb  4 12:26:00 1985


      It is possible to detect dereferencing of null pointers statically
for many programs, and language restrictions making this work are quite
possible.  But here you enter the strange and wonderful world of mathematical
proof of correctness.  It is very painful to write verifiable programs; imagine
someone looking over your shoulder insisting that you justify formally every
pointer reference.  Still, it is a way to rock-solid code.  See my ``Practical
Program Verification'', Proc. ACM POPL, 1983.

					John Nagle