ogden@seal.cis.ohio-state.edu (William F Ogden) (06/25/91)
In article <6375@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) writes: >>>Any semantic problems that were ever associated with gotos remain in full >>>force when you use procedure calls. >> (I assume this isn't a call for reviving the GoTo :-) >I don't see why you're assuming anything. Read my lips: Goto is not dead. I'll certainly try to avoid those unwarranted assumptions now. >> Procedures which >> have explicit parameters and don't side-effect global variables are >> semantically simpler than GoTo's and Labels. >I'm sorry, but this turns out not to be the case. Let me repeat the >sentence above: > ANY semantic problems that were ever associated with gotos > [insertion: gotos in fact have *very* simple proof rules] > remain in FULL force when you use procedure calls > [insertion: in fact proof rules for procedure calls are > MORE complex than proof rules for labels and gotos.] It is true that the early claim that there was no proof rule for labels and goto's while there were simple ones for the structured control constructs was quite specious. As you note, the rules for labels and goto's are really quite simple _in form_. You just attach a global invariant to each label and make sure the appropriate invariant is satisfied at each goto. However, if you actually try to use these rules, you soon discover that simplicity in rule form does not guarantee simplicity in the resulting program verifications. The problem here turns out to be that the label invariants must precisely describe the entire global state and are consequently elaborate and difficult to formulate. In addition, these complex invariants are messy to verify at each goto. In contrast, the proof rules for procedure declarations and calls are slightly more elaborate in form, but since actual usage normally only involves a small number of procedure parameters (the narrow interface), the pre and post conditions must only describe the relationship among a a few variables rather than the relationship among all the variables in the system. So the pre and post conditions are simpler to formulate, smaller, and result in less complex proofs. >This is not a theoretical abstraction. I have noticed, IN PRACTICE, >that when reading a couple of hundred lines of functional code (which >I like, make no mistake) I get the same sensation as when I used to >read assembly code. There is one great big mass of spaghetti, and >unsnarling references to functions (when every second line defines >a new function) is not one iota easier than unsnarling references to >labels. It is certainly true that procedures (like most other mechanisms) can be used to create an incomprehensible mess. As Dijkstra pointed out 20 odd years ago and object oriented partisans have reiterated, we should view procedures as a mechanism for creating operations on virtual objects, not as a mechanism for aggregating random snippets of code. If this is done properly, then the procedures effect simply described, easily remembered operations on the virtual objects. (This abstraction process also simplifies proofs of programs, since it permits the proof to be carried out in a higher level domain where assertions are much simpler and more concise.) If you have to unsnarl calls to procedures or read code to figure out what a procedure does, then something is definitely wrong. The point here is that procedures _can_ be used to simplify the semantics of programs, while goto's generally can not. >>Now the fact that a compiler hides the low-level jump statement and only >>uses it in safe ways is precisely the point of a good high-level abstraction. >You have missed the point completely. The point is that the difficulty >with gotos was not that they were theoretically unclean (quite the >opposite! I repeat, the proof rules for (local) goto are SIMPLER than >the proof rules for procedure call) but that you had to do a lot of >moving your finger around a listing and mumbling to yourself to figure >out what came from where. The hardware jump was never the problem, it >was figuring out what the connection between a particular jump and a >particular label MEANT. It would somehow be wrong to view this as an argument supporting the semantic complexity of goto's, no doubt. >>The user of higher level control constructs really lives in a semantically >>simpler and safer world. >This turns out not to be the case. *Anything* you could do with labels >can be done IN THE SAME WAY (I mean preserving apparent structure, size of >output of transliteration process is a linear function of size of input) >using function calls. This has been known since the early 60s, where have >you been? Why back in the early 60's we used to write self-modifying code, which fortunately isn't easy to transliterate. (I hesitate to presume, but surely you don't advocate self-modifying code.) :-) Now the line of argument here seems to be that since say a Volvo can do anything that a model T could, then the Volvo is no more simple or safe to use than a model T. [By the way, if you insist on side effect free procedures, your transliteration process will turn out to be quadratic in the length of a program, since you have to pass around the entire state space.]