🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.specification
Article #195

Re: specifying OBJ in itself

#195
From: leland.f.derbenwick
Date: Fri, 12 Oct 1990 17:28
63 lines
3847 bytes
In article <1990Oct11.115952@julien.informatik.uni-dortmund.de>,
angelica@julien.informatik.uni-dortmund.de (Angelica M. Kappel) writes:
  [ regarding specifying OBJ3 in itself ]
>  Unfortunately, it turned out that the implementation
> of OBJ3 
> is slow and used too much space on our machine (SUN 3/50). Our
> specification grew too big
> to be executable.

This appears to be a general problem with any executable specification
system.  A good _specification_ is optimized for readability and
understandability.  To do this for a complex system, we build a layered
specification in which primitive objects are specified, then more
complex ones based on the primitive objects, then still more complex
objects, until we have specified the entire system.

But an executable specification must also meet some minimal performance
(memory space and/or execution time) requirements to be useful.  It's
not executable in any meaningful sense if the real system is
implemented, delivered, and replaced by a successor before the suite of
proposed test cases has been validated by cranking them through the
specification simulator.

But each additional layer of specification increases the execution time.
_At some point_, it's no longer practical to execute it.  This usually
happens just when the specification is big enough to be interesting.  :-(

There's one "easy" fix for this, but I think the cure is worse than the
disease.  It is _very_, _very_ tempting to start rewriting the lower
levels of the specification in order to make them more efficient.

A slightly cheesy example:  "But I only made the cheddar spec a little
bit more complicated, and now I can run my test cases against the
gorgonzola in only 10 minutes instead of two days."  And then the swiss
spec and the mozzarella spec get rewritten to improve _their_ speed,
and the cheddar spec gets rewritten again to tweak it a bit more, and
pretty soon the whole mess is totally incomprehensible to everyone but
(maybe) its developers.

All this rewriting has destroyed the spec for its _original_ purpose,
which was to precisely describe the desired behavior in a rigorous and
understandable fashion.

Allowing the lower level specs to be replaced by actual implementations
for execution purposes is better, since the spec itself isn't corrupted.
But there is still a problem, because now the specification implicitly
becomes the design for the real system.  So implementation details start
showing up in the spec, and the _purpose_ of the spec has been corrupted.

I don't know any easy answers to these problems; I now tend to see
executable specifications as more likely part of the problem than of the
solution.

If you're still reading after all this, I covered quite a bit of this in
my dissertation: Leland F. Derbenwick, "Formal Specification of Module
and Resource Behavior During Software Design." Ph.D. Dissertation,
The University of Connecticut, 1985.  It's available from University
Microfilms in Ann Arbor, Michigan, and if enough of you order it all at
once, they even promised to send me a couple bucks in royalties!  :-)  :-)

 -- Speaking strictly for myself,
 --   Lee Derbenwick, AT&T Bell Laboratories, Warren, NJ
 --   lfd@cbnewsm.ATT.COM  or  <wherever>!att!cbnewsm!lfd
Technical Details
Message-ID: <1990Oct12.172820.4771@cbnewsm.att.com>
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!sdd.hp.com!decwrl!shelby!rutgers!att!cbnewsm!lfd
References: <6470@vanuata.cs.glasgow.ac.uk> <1990Oct11.115952@julien.informatik.uni-dortmund.de>

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!sdd.hp.com!decwrl!shelby!rutgers!att!cbnewsm!lfd
From: lfd@cbnewsm.att.com (leland.f.derbenwick)
Newsgroups: comp.specification
Subject: Re: specifying OBJ in itself
Summary: Executable specifications considered harmful...
Message-ID: <1990Oct12.172820.4771@cbnewsm.att.com>
Date: 12 Oct 90 17:28:20 GMT
References: <6470@vanuata.cs.glasgow.ac.uk> <1990Oct11.115952@julien.informatik.uni-dortmund.de>
Organization: AT&T Bell Laboratories
Lines: 63