jack@cs.glasgow.ac.uk (Jack Campin) (10/03/90)
Has anybody tried to specify an algebraic specification language, like OBJ3, in itself? -- -- Jack Campin Computing Science Department, Glasgow University, 17 Lilybank Gardens, Glasgow G12 8QQ, Scotland 041 339 8855 x6044 work 041 556 1878 home JANET: jack@cs.glasgow.ac.uk BANG!net: via mcsun and ukc FAX: 041 330 4913 INTERNET: via nsfnet-relay.ac.uk BITNET: via UKACRL UUCP: jack@glasgow.uucp
angelica@julien.informatik.uni-dortmund.de (Angelica M. Kappel) (10/11/90)
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
lfd@cbnewsm.att.com (leland.f.derbenwick) (10/13/90)
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