🚀 go-pugleaf

In article <6470@vanuata.cs.glasgow.ac.uk>, jack@cs.glasgow.ac.uk (Jack
Campin) writes:
|> Has anybody tried to specify an algebraic specification language,
like
|> OBJ3, in itself?

We had a project group called BASTA in 1988/89 where we did 
exactly what you are looking for.
We specified mainly narrowing and rewriting in OBJ3 (including
order-sorted 
rewriting but without module system). An algebraic specification can be
given in form
of rewrite rules. 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.

There exists a report of the group BASTA at the University of Dortmund
(in German):
"Endbericht der PG BASTA - Basissystem f"ur Termersetzung und
automatisches Beweisen,
SS 1988 - WS 1988/89" . The sources are completely listed there.
Anyone who is interested may contact the following address:

               BASTA
               Lehrstuhl Informatik 5
               Universit"at Dortmund 
               Postfach 500500
               4600 Dortmund 50
               Renunited States of Germany

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

In article <1990Oct12.172820.4771@cbnewsm.att.com> lfd@cbnewsm.att.com
(leland.f.derbenwick) writes:

 > 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.

The following paper makes a number of points against executability of
specification languages:

   @Article(      HJ_89,
    Author=      "I. J. Hayes and C. B. Jones",
    Title=       "Specifications are not (necessarily) executable",
    Journal=     "Software Engineering Journal",
    Year=        "1989",
    Month=       nov,
    Pages=       "330--338")


Oliver Schoett	     Institut f. Informatik, Technische Univ. M"unchen
		     Postfach 20 24 20,	   8000 M"unchen 2,    Germany
schoett@informatik.tu-muenchen.dbp.de		      +49 89 2105 2390
schoett%informatik.....de@  {relay.cs.net, unido.uucp, dfngate.bitnet}

schoett@informatik.tu-muenchen.dbp.de (Oliver Schoett) writes:

>The following paper makes a number of points against executability of
>specification languages:

The primary reason from avoiding executable specification languages is
that it is sometimes necessary to discuss problems outside of the realm
of computable functions. An important example of this is specifying the
termination of a program.

--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       
Department of Computer Science   | heretic: someone who disgrees with you
University of Queensland         | about something neither of you knows
Australia                        | anything about.

In article <5289@uqcspe.cs.uq.oz.au> brendan@batserver.cs.uq.oz.au writes:
>schoett@informatik.tu-muenchen.dbp.de (Oliver Schoett) writes:
>
>>The following paper makes a number of points against executability of
>>specification languages:
>
>The primary reason from avoiding executable specification languages is
>that it is sometimes necessary to discuss problems outside of the realm
>of computable functions. An important example of this is specifying the
>termination of a program.
>
Why would you need to be able to specify divergent programs? 
What possible computational interpretation would such a specification
correspond to? 

>--
>Brendan Mahony                   | brendan@batserver.cs.uq.oz       
>Department of Computer Science   | heretic: someone who disgrees with you
>University of Queensland         | about something neither of you knows
>Australia                        | anything about.

yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:

>Why would you need to be able to specify divergent programs? 
>What possible computational interpretation would such a specification
>correspond to? 

No you want to be able to specify that it does not diverge! You can't do
this in any executable notation.

--
Brendan Mahony                   | brendan@batserver.cs.uq.oz       
Department of Computer Science   | heretic: someone who disgrees with you
University of Queensland         | about something neither of you knows
Australia                        | anything about.

In article <5321@uqcspe.cs.uq.oz.au> brendan@batserver.cs.uq.oz.au writes:
>yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:
>
>>Why would you need to be able to specify divergent programs? 
>>What possible computational interpretation would such a specification
>>correspond to? 
>
>No you want to be able to specify that it does not diverge! You can't do
>this in any executable notation.
>

In a well defined executable notation, you should only be able to specify
systems that will not diverge. That is, construction of a specification
should itself constitute a proof that the specified system is non
divergent.