Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!wuarchive!uunet!stanford.edu!msi.umn.edu!umeecs!dip.eecs.umich.edu!warack From: warack@dip.eecs.umich.edu (Christopher Warack) Newsgroups: comp.software-eng Subject: Re: Modifiability Message-ID: <1991Jun10.122656.18795@zip.eecs.umich.edu> Date: 10 Jun 91 12:26:56 GMT References: <11714@ncar.ucar.edu> <1991Jun7.165928.1903@weyrich.UUCP> <1849@uqcspe.cs.uq.oz.au> Sender: usenet@zip.eecs.umich.edu (Mr. News) Distribution: comp.software-eng Organization: University of Michigan EECS Dept. Lines: 63 In article <1849@uqcspe.cs.uq.oz.au> anthony@cs.uq.oz.au writes: >In <1991Jun7.165928.1903@weyrich.UUCP> orville@weyrich.UUCP (Orville R. Weyrich) writes: >>The problem with this is that the specification becomes to all intents and >>purposes the programming language, and if Ada or C (or something else) is ************************ >>later generated automatically from this specification, its just an intermediate >>pass of a huge compiler. > >>In effect, the specification language becomes the language in which the >>source code is written. > >I disagree, there are two problems with trying modify a software from a >natural language specification. > >1. The specification is most likely to be ambigious and the >designer of the modification has to make the best **guess**. I think we're seeing two ways of looking at this problem. Yes, the spec could be ambiguous. I don't believe Balzer "required" full automation; programmer interaction during the code generation phase, guided by automation, was the plan. But, if you take the other position that the spec is not ambiguous, then you need something as rich as the program written in a HOL to describe it. If the code is not necessary, why was it in the program to begin with. There is some amount of code "infrastructure" such as setting up the execution environment or manually implementing high-level structures such as exceptions that could probably be ignored in a specification. I'd assert, however, that more than 95% of a reasonably sized program's code is an attempt at writing a non-ambiguous specification. 1/2 :-) >2. It is very difficult for the designer of the modification >to figure out the effect of his modification on the existing >software. Formal specification is more than just a higher level >programming language. It allows the designer of the modification >to reason about the effects of his modification on the rest of >the system. I believe that designers of programming languages also desire this ability...??? While simplification of a problem may make it easier to reason about, it may also tend to hide the characteristics/ behavior that cause the problem. >Furthermore you have to consider that the modification could have >taken place several months after the delivery of the original >product (or even years). How can you guarantee that the source >code of the original product would be available. As easily as guaranteeing that the formal specification is available. >Even if the source code was availabe it far more difficult to analysis >for conflicting properties between existing software and new software >at the source level. than what? at the object level? Formal specification techniques of the kind that Balzer proposed don't exist yet, so you can't mean those, can you? -- Chris >-- >Anthony Lee (Michaelangelo teenage mutant ninja turtle) (Time Lord Doctor) >email: anthony@cs.uq.oz.au TEL:+(61)-7-365-2697 (w) >SNAIL: Dept Comp. Science, University of Qld, St Lucia, Qld 4072, Australia