Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uwm.edu!cs.utexas.edu!tut.cis.ohio-state.edu!elephant.cis.ohio-state.edu!weide From: weide@elephant.cis.ohio-state.edu (Bruce Weide) Newsgroups: comp.sw.components Subject: Re: Seeing component source code? Message-ID: <73104@tut.cis.ohio-state.edu> Date: 25 Oct 89 22:08:00 GMT References: <67790@tut.cis.ohio-state.edu> <130200016@p.cs.uiuc.edu> Sender: news@tut.cis.ohio-state.edu Reply-To: Bruce Weide Organization: Ohio State University Computer and Information Science Lines: 95 Ralph Johnson's recent comments about the differences between specification and implementation call for a few more comments and questions of clarification. (1) Ralph gives an example of a simple implementation of stacks and simple algebraic specification, and concludes: "The second (the "abstract" specification) is shorter, but not much easier to read. Most importantly, it is not easier to understand. Thus, I claim it is no better as a specification than the first." I'm not sure I understand the point of this example, except that it is POSSIBLE for an implementation to be about as short and as simple as its formal specification. No argument there. But the claim that the algebraic specification is "THE abstract specification" is too strong. There are other well-known specification methods that, we would both apparently agree, render specifications easier to comprehend than the algebraic approach. Such specifications remain abstract but do not rely on using equations, as in Ralph's example. Such alternative specification methods should result in easier-to-understand specifications of stacks. Admittedly these alternatives might look on the surface very much like Ralph's source code (for this example but not in general). But they are subtly and importantly different in meaning precisely BECAUSE they are abstract. One might, for example, use a mathematical sequence as a mathematical model of a stack. But there would be no implication that program sequences are used in the implementation, as apparently Ralph has done in his code. This is important for lots of reasons, upon which I can elaborate if the discussion continues along this line. (2) Ralph continues: "Stacks are about the easiest component for which one can write a formal specification. However, a better example to show the strengths of formal specifications would be sorting, since the specification is that the output sequence is a permutation of the input sequence and that the output sequence is sorted, while most fast sorting algorithms take a lot of more code to express. This is an example of a problem for which there exists both fast complex algorithms and slow simple algorithms. The specification I described corresponds to the sorting algorithm that takes each permutation and checks whether it is sorted. This simple specification could be represented just as well by a program." The general claim here seems to be that for a reusable component with a compact formal specification, there is also a simple but possibly inefficient ALGORITHM that is its implementation and that, to some people at least, would be easier to understand. This seems unlikely at best. Consider a simple example. Suppose you have a component that keeps track of a function from some domain type D to some range type R (both parameters to the component). You want to specify a boolean-valued operation that returns "true" given f and r iff function f maps some value of type D to the specific value r. This is easy to specify in the abstract using an existential quantifier; something like: there exists d:D such that f(d) = r Presumably the source code to explain this behavior consists of a program to search through all values of type D for one that f maps to r. Two problems here. First, D may not be finite, in which case this is not an algorithm at all because it may not terminate and could never return "false". Second, how do you write this program (except in pseudocode or something) without knowing what type D is? But Ralph has provided a good idea here: to challenge specification writers to design and specify a component that permits one to do sorting. I'm happy to oblige, and will post such specs to this forum if asked to do so. But we should also be able to see the "simple specification" mentioned in the last sentence above for comparison purposes relative to ease of understanding. A biased audience, readers of this forum, but we might get some info nonetheless. Of course, comparisons on other grounds (e.g., ease of verification that alternative implementations meet the specs; whether the spec method helps one design a good reusable component in the first place; lots of other questions) might be too difficult to carry out in this forum. But it would be a start at seeing whether people might prefer to see source code or formal specifications for their reusable components. -Bruce ------ Prof. Bruce W. Weide Dept. of Computer and Information Science The Ohio State University 2036 Neil Ave. Mall Columbus, Ohio 43210-1277 USA Phone: 614-292-1517 E-mail: weide@cis.ohio-state.edu