Path: utzoo!utgpu!watserv1!watmath!att!ucbvax!tut.cis.ohio-state.edu!elephant.cis.ohio-state.edu!weide From: weide@elephant.cis.ohio-state.edu (Bruce Weide) Newsgroups: comp.software-eng Subject: Re: Reuse and Abstraction (was: reu Message-ID: <81153@tut.cis.ohio-state.edu> Date: 4 Jun 90 14:55:48 GMT References: <4979@stpstn.UUCP> <102100009@p.cs.uiuc.edu> <19820@duke.cs.duke.edu> <12085@june.cs.washington.edu> <81111@tut.cis.ohio-state.edu> <5152@stpstn.UUCP> Sender: news@tut.cis.ohio-state.edu Reply-To: Bruce Weide Organization: Ohio State University Computer and Information Science Lines: 60 In article <5152@stpstn.UUCP> cox@stpstn.UUCP (Brad Cox) writes regarding whether formal specifications are a pain: >-------- > >"Most" people (certainly not myself) aren't saying that they're a big pain >for stacks. A lot of them *are* saying that their usefulness is less obvious >than their costs for bigger objects like Sets (see Ralph London's article), >word processors, or hamburgers. > >-------- We've written the formal spec for a set module, too, and it's awfully easy to write the spec once you have decided on a design of the intended abstract behavior. (This may sound trivial but it is not if reuse is an issue.) We've also written quite comprehensible formal specs for lots of other concepts, too, including partial functions (for associative searching), graphs, etc., and have been teaching them to undergraduates and to practicing software engineers in industry for several years. In fact, the spec for a set module has been a favorite exam question. So this notion that stacks are the only things people can specify formally (yet still comprehensibly) is just plain bogus. It is to be expected that a formal spec for a word processor is going to be rather formidable, even AFTER you have figured out what it is and how it is supposed to behave from an abstract viewpoint. But this difficulty can hardly be attributed to the desire to make the specification formal. Do you have something you'd call an acceptable "rigorous" specification of a word processor? I'd be surprised if it couldn't be stated formally with just about the same number of symbols, and if the formal spec wasn't just about as readable to someone who has learned to read a formal specification. Besides, I'll let you attach an informal and/or rigorous spec to the formal one if you think it will help people understand what's going on. A formal spec can include natural language comments. The comments just won't be machine-processable and won't participate in correctness proofs any more than comments in code participate in code generation. What I'm suggesting is that formality is not much more expensive than rigor. It may pay off big-time in the long run precisely because of reuse. Reuse of components demands that the client understand WHAT a reusable component is supposed to do, and that the client be confident that the implementation he/she is buying actually does it. Formality makes the first objective feasible if people can learn how to read formal specs; everyone doesn't have to be an expert in writing them. And if formally specified components are reused, the cost of formal verification of correctness of implementations can be amortized over many future uses. I'm not saying there's no place for informality in software, just that we should not overlook places where formality can help, nor the possibility of (re)using some of the work that mathematicians have been so kind to do for us. Let me not discuss the formal specification of a hamburger, because all I'm arguing for is formal specification of software components. I never claimed the technique would or should be applied to everything in the world... Although living in the home of Wendy's and a variety of other fast food chains, maybe I could tap into some local industrial support if I could adapt the method to burgers. Hmmm... -Bruce