Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!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: <1991Jun12.115602.4153@zip.eecs.umich.edu>
Date: 12 Jun 91 11:56:02 GMT
References: <1849@uqcspe.cs.uq.oz.au> <1991Jun10.122656.18795@zip.eecs.umich.edu> <1893@uqcspe.cs.uq.oz.au>
Sender: usenet@zip.eecs.umich.edu (Mr. News)
Distribution: comp.software-eng
Organization: University of Michigan EECS Dept.
Lines: 85

I don't know what exactly happened here; but it's some kind of context
switch.  I thought this piece of thread had headed off into the topic of
automatic programming where the program is generated "mechanically" from
the specification.  I argued that this requires a spec to be nearly as
complex as the implementation.  Thus, eliminating real improvement over
traditional HOL implementation (except in certain well-understood
application areas).  This is NOT the spec that comes with a contract.  If
it is, why is the customer letting a contract, they've already done the
work.

I agree completely that specs should address maintainability concerns.
This issue is independent of formal/non-formal and automatic programming
arguments except to the extent that they may make it easier to specify
maintainability concerns.  I haven't seen any clear advantage in any
of them.

Furthermore, I have absolutely no qualms about the "traditional" approach
which states you should maintain your spec and design as well as your code.
Abstraction is good and should be maintained.  I also understand why this
doesn't happen all that often.  In fact, it's quite possible that formal
specs may make this easier, since one of the big problems with abstraction
maintenance is "traceability."  A good formal method should relate better
to the implementation and be more traceable.

Just trying to keep the swap space clean :-)
-- Chris

In article <1893@uqcspe.cs.uq.oz.au> anthony@cs.uq.oz.au writes:
>In <1991Jun10.122656.18795@zip.eecs.umich.edu> warack@dip.eecs.umich.edu (Christopher Warack) writes:
>
>>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 :-)
>
>That is true the program's code is itself a specification.  The problem
>of modifiability depends on the level that we are working on.  
>However if we don't deal with problem of modifiability at the specification
>level then they don't go away at the implementation level.  This means
>that not only do you have deal with implementation issues that will
>affect modifiablity but you also have to deal with specification issues
>that is being carried forward because you didn't bother with them 
>at the specification level.
>
>>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.
>
>Again, I point out that modifiability problem at the high level
>don't just go away at the implementation level.  If you can knock
>those problems over the head at the specification level then the 
>problem at the implementation level would be easilier to deal with.
>
>>>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.
>
>Most companies are very reluctant to hand over code but the specification
>is alway part of the contract.  In fact it is the contract. 
>If we insist that the contract be written formally then we will always
>have it with us. 
>
>
>>>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
>--
>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