Path: utzoo!attcan!uunet!munnari.oz.au!uhccux!ames!think!zaphod.mps.ohio-state.edu!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: <81111@tut.cis.ohio-state.edu> Date: 1 Jun 90 21:14:54 GMT References: <4979@stpstn.UUCP> <102100009@p.cs.uiuc.edu> <19820@duke.cs.duke.edu> <12085@june.cs.washington.edu> Sender: news@tut.cis.ohio-state.edu Reply-To: Bruce Weide Organization: Ohio State University Computer and Information Science Lines: 68 In article <12085@june.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes: >----- >I can't resist responding to comments by Charlie Martin, Bruce Weide, >Brad Cox and maybe others too (I can no longer untangle who said what): >... > >> A specification is "formal" if it ... can be used to verify the correctness >> of ... an implementation ... > >Emphasis on verification of implementations excludes a lot of what formal >specifications are about. Often you need to reason about the properties of >some proposed system, and this is a prerequisite to deciding if you want to >implement the specified behavior at all. Formal specifications may make it >possible to reason about system behavior by applying rules of inference (as >opposed to building an implementation and experimenting with it). For example, >you might want to show that some proposed collection of operations cannot >violate particular assertions about safety. This is an entirely separate >issue from verification and is independent of any particular implementation. >----- FYI, I made the original statement about what I'd consider a "formal specification" as opposed to a "rigorous specification." I agree, of course, that one can use formal statements to "reason about the properties of some proposed system." In fact, the ability to do this before you implement the specified software was one of the three specific criteria I offered for deciding whether you had a "formal specification." It is not "an entirely separate issue from verification" because it is exactly at the heart of verifying that the CLIENT of the not-yet-implemented system will behave as expected. Therefore, I'm not sure how your point relates to the proposed definition of what should be called a "formal specification." If you're saying that we should call something a "formal specification" even if it doesn't COMPLETELY describe the intended behavior, then we agree there, too. It is possible for a formal specification to permit tremendous latitude in the implementation. For example, if you want to say that the following is a specification of the behavior of the effect of a "push" operation on a stack s: length(s) = length(original s) + 1 then you'd better be willing to accept lots of weird, non-stack-like implementations. The point is that just calling it a "stack" doesn't mean a thing. If you want intuitive stack-like behavior you have to ask for it in the specification. If all you want to do is reason about the lengths of stacks then your specification is fine, but again, don't blame me if I implement a FIFO queue or something. If your reasoning depends on me providing you with code that implements a stack (as you intuitive expect it to behave) you'll have to say so explicitly. And this seems to have nothing to do with the distinction between formalism and rigor, unless use of the word "stack" is somehow considered rigorous enough. This gets to Brad Cox's point about "common sense." I guess the above example helps illustrate where Brad and I might disagree (if I understand the argument he's making). Brad seems willing to describe the intended behavior of stacks by saying the implemented objects "act like stacks" and relying on my common sense to understand what he means. As I've pointed out before, though, even THIS seemingly rather precise statement means different things to different people. It's not that hard to say it rigorously, and (IMHO) no harder to say it formally than rigorously. I still don't understand the resistance to doing so. People keep implying or explicitly stating that formal specs are inherently such a pain, but why? -Bruce