macrakis@harvard.ARPA (Stavros Macrakis) (01/29/85)
> > For instance, it is possible to statically guarantee that nil > > pointers are never dereferenced --Pemberton > Ada supports this... --Steinman Unfortunately, this is not and cannot be true. (consider "a := if program P halts, then nil else new foo; deref(a)") What Ada could have done and didn't would be to define a subtype of access types `non-null'; no dereferences of a variable of such subtype would need be dynamically checked, but of course assignments to values not of that subtype would have to be. Such a subtype would probably make possible the elimination of essentially all dynamic nil deref checks in many programs, if properly used. -s Appendix: Example type ptr is access foo; subtype goodptr is ptr.all; -- Arbitrary syntax; suggests .all exists XXX v: goodptr; --Illegal: default initialization is nil v,w: goodptr := new foo; x,y: ptr; function ptrptr(a:ptr) return ptr; function ptrgoodptr(a:ptr) return goodptr; function goodptrptr(a:goodptr) return ptr; ... v := x; -- Must check for non-null w := v; -- Check not necessary v := ptrptr(v); -- Must check result v := ptrgoodptr(v); -- No checks necessary x := goodptrptr(v); -- "
steven@boring.UUCP (01/30/85)
Jim Davies@uiucdcsb.UUCP writes: > boring!steven states that it is possible to statically insure that nil > pointers are never dereferenced. The following program provides a simple > counterexample to this claim: [a Pascal program followed] and macrakis@harvard.ARPA (Stavros Macrakis) writes: > > > For instance, it is possible to statically guarantee that nil > > > pointers are never dereferenced --Pemberton > > Ada supports this... --Steinman > > Unfortunately, this is not and cannot be true. (consider "a := if > program P halts, then nil else new foo; deref(a)") Of course you can't do it without extra syntax! But strong typing is also impossible (consider int a; a:= if P halts then "hello" else 123). The point is, that it is possible to define a language so that it is possible statically to guarantee that nil is never dereferenced (Stavros's Ada example contains the germ of the idea). You can't do it in Vanilla Pascal or C. Steven Pemberton, CWI, Amsterdam; steven@mcvax.
macrakis@harvard.ARPA (Stavros Macrakis) (01/31/85)
> > > ... > > ... > The point is, that it is possible to define a language so that it is > possible statically to guarantee that nil is never dereferenced. > ... -- Steven Pemberton, CWI, Amsterdam; steven@mcvax. Yes, yes, agreed that you can do this, but only if there is no nil in the ordinary sense (since you use the word `nil', presumably there must be a nil!). Instead, you use access types with no nil and some other mechanism (such as a union type or variant record), or you use tricks like circular lists (or is there some better way?). In the first case, the dynamic check for nil is replaced by a dynamic check for the right variant (is that any different?); in the second, it is replaced by obscure code (which is likely to replace dereferencing nil with incorrectly terminating at the end of lists...!). In any case, there is runtime cost and runtime notification of the error, not compile time. Perhaps unions or variants are cleaner than nil's, but they don't eliminate the dynamic checks. Dynamic checks are fine with me. A more radical approach simply eliminates pointers altogether...and relies instead on higher-level concepts--but let me not digress. But I do fully agree with Pemberton's original point, that languages and language tools should support the programmer as much as possible: the costs are surely negligible compared to the additional safety. -s PS This whole chain of responses could presumably have been avoided if Pemberton had been a bit less mysterious about his remark on static checking. (A stitch in time saves nine?)
bobo@inmet.UUCP (01/31/85)
> > > For instance, it is possible to statically guarantee that nil > > > pointers are never dereferenced --Pemberton > > Ada supports this... --Steinman > Unfortunately, this is not and cannot be true. (consider "a := if > program P halts, then nil else new foo; deref(a)") Excuse me for putting words into Mr. Pemberton's terminal but I think that what he was trying to say was NOT that you can guarantee that a nil dereference WILL occur, but that it WILL NOT occur. In the above example a compiler can warn you that a nil dereference MAY occur. In many situations this information can help you to discover bugs. In other situations you may just say "so what."
ndiamond@watdaisy.UUCP (Norman Diamond) (02/04/85)
> > > > For instance, it is possible to statically guarantee that nil > > > > pointers are never dereferenced --Pemberton > > > Ada supports this... --Steinman > > Unfortunately, this is not and cannot be true. (consider "a := if > > program P halts, then nil else new foo; deref(a)") [--?] > Excuse me for putting words into Mr. Pemberton's terminal but I > think that what he was trying to say was NOT that you can guarantee > that a nil dereference WILL occur, but that it WILL NOT occur. > In the above example a compiler can warn you that a nil dereference > MAY occur. In many situations this information can help you to > discover bugs. In other situations you may just say "so what." [--bobo(?)] In that case, nearly every dereferencing operation in the source program will draw that warning message. Of course, programmers would have to ignore the warnings, and their content of usable information would be near zero. -- Norman Diamond UUCP: {decvax|utzoo|ihnp4|allegra|clyde}!watmath!watdaisy!ndiamond CSNET: ndiamond%watdaisy@waterloo.csnet ARPA: ndiamond%watdaisy%waterloo.csnet@csnet-relay.arpa "Opinions are those of the keyboard, and do not reflect on me or higher-ups."
jbn@wdl1.UUCP (02/05/85)
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