🚀 go-pugleaf

Hello everybody,

a few days ago I asked some questions about algebraic specification.
The answers were the best I ever received on a news query -- compliments
to the members of this newsgroup !
Here are the questions and the essence of the answers to them:

1. How can I check whether my axioms really cover the functionality 
   I have in mind ?  I know that this can not be done formally.

[[ Two methods: Think of some formal properties the axioms should 
                entail and try to prove them from the axioms
            OR  Get a specification execution tool, play around with
                your specification and look whether it does what you
                expect.
]]                

2. How can I check whether I have redundant axioms ?

[[ Try to prove each axiom that you suspect to be redundant from
   the other ones.
]]

3. How can I check whether two given specifications are equivalent ?

[[ For specifications without isomorphic signatures, this is difficult
   to formalize. Otherwise, try to prove one set of axioms from the 
   other set and vice versa.
]]
   

4. How can I check whether one specification subsumes another,
   i.e., the first datatype can emulate the second ?

[[ Again, this is difficult to formalize unless the signatures are
   isomorphic. (E.g. of course you can emulate a stack with a linked
   list -- but what exactly does ``emulate'' mean in general ?)
   For isomorphic signatures the set of axioms of the subsuming 
   specification implies the set of axioms of the subsumed specification.

5. Are there any tools that support working with algebraic 
   specification ?  How good are they ?  Prolog, Lisp ?

[[ Well, er, there are some, ...but, hm, see below ]]

All answers that involve proof steps indicate that the problem is
undecidable in general.

There were also some pointers to the literature.

Thanks to all who replied

  Lutz
  
Lutz Prechelt   (email: prechelt@ira.uka.de)            | Whenever you 
Institut fuer Programmstrukturen und Datenorganisation  | complicate things,
Universitaet Karlsruhe;  D-7500 Karlsruhe 1;  Germany   | they get
(Voice: ++49/721/608-4317, FAX: ++49/721/694092)        | less simple.
 

---------------------------------------------------------------------------
Here are the (slightly edited) complete answers I received:
---------------------------------------------------------------------------
Date: Thu, 22 Oct 92 18:03:13 BST
From: areid <areid@dcs.gla.ac.uk>

In comp.specification you ask:

First some brief replies, then some references. (btw, most of these
problems are, in general, insoluble.)

>1. How can I check whether my axioms really cover the functionality 
>   I have in mind ?  I know that this can not be done formally.

Term rewriting (sort of semi-auto transform to a sort-of program) can
sometimes make the specification executable.

There is also a formal notion of "completeness" which just checks that
the result of every visible computation is fully specified. 

>2. How can I check whether I have redundant axioms ?

Who cares if they're redundant?
(If you decide you do, try proving a redundant-looking axiom from the
remainder.)

>3. How can I check whether two given specifications are equivalent ?

Try proving all axioms of spec1 follow from axioms of spec2 and
conversely.

This gets hard with structured specifications!

>4. How can I check whether one specification subsumes another,
>   i.e., the first datatype can emulate the second ?

Depends on your definition (eg you could argue that arrays subsume
stacks since you can implement stacks using arrays.)

If you mean two specs with same signature, you could think about
whether "subsumes" means weaker. If so, try showing that each axiom of
spec1 follows from the axioms of spec2.

>5. Are there any tools that support working with algebraic 
>   specification ?  How good are they ?  Prolog, Lisp ?

Hopefully someone more tool-oriented will answer this. If not, mail me
back and I'll see if I have any info.


OK, some references for this. (nb these are usually quite old so they
are about "initial semantics". If you are wanting to work on
implementing specifications, more recent work on "loose" or
"ultraloose semantics" is more appropriate - but I can't think of any
approprioate references offhand.)

I'm not sure which (if any) of these are relevant but they're a place
to start and I think they do discuss the issue. The paper I was really
looking for an online reference for was "Do not write more axioms than
you have to" but I don't remember the author. If you prod me, I can
probably find it amongst my papers. Also, P. Padawitz (from Berlin I
think?) did some work on consistency (is spec too strong) or
completeness (is spec too weak) in the early eighties but again I
don't have an on-line reference.


%A John V. Guttag
%T Abstract Data Types and the Development of Data Structures
%J |COMMA1|
%V 20, 6
%D |JUN| 1977
%P 396--404

%A John V. Guttag
%A J. J. Horning
%T The Algebraic Specification of Abstract Data Types
%J |ACTAI2|
%V 10
%D 1978

%A John V. Guttag
%T Notes on type abstraction
%P 593--616
%J |LNCS69|


%A John V. Guttag
%A E. Horowitz
%A D. R. Musser
%T The Design of Data Type Specifications
%P Chapter 4
%E Yeh\
%B Advances in Computer Programming\
%V 4\
%D 1978
---------------------------------------------------------------------------
Date:     Fri, 23 Oct 92 15:32:23 MET
From:     "Norbert Runge, IPD, UniKA" <runge@ira.uka.de>

Hallo Lutz, 

hier noch die angekuendigte Literatur:

@ARTICLE(GuHo,
         AUTHOR  = "J.V.Guttag and J.J.Horning",
         TITLE   = "The Algebraic Specification of Abstract Data Types",
         JOURNAL = "Acta Informatica",
         YEAR    = 1978,
         PAGES   = "27-52")

@ARTICLE(BeTh,
         AUTHOR  = "Alfs T. Berztiss and Satish Thatte",
	 TITLE   = "Specification and Implementation of
	            Abstract Data Types",
         JOURNAL = "ADVANCES IN COMPUTERS",
	 VOLUME  = 22,
	 YEAR    = 1983,
	 PAGES   = "295-353",
	 NOTE    = "Umfassende Einfuehrung in das Gebiet der ADT's.
	            Stellenweise allerdings etwas sehr kompakt und daher
		    recht schwer verstaendlich. Umfassende Bibliographie.")
---------------------------------------------------------------------------
Date: Fri, 23 Oct 92 14:51:05 -0400
From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>

1. How can I check whether my axioms really cover the functionality 
   I have in mind ?  I know that this can not be done formally.

	You can try formulating some properties that you believe your axioms
	entail, and then try proving these properties from the axioms.

2. How can I check whether I have redundant axioms ?

	You can try proving each axiom from the others.  Equivalently, you can
	replace the axioms one at a time with their negations and try proving a
	contradiction (if you get one, that means the axiom in question is
	redundant).

3. How can I check whether two given specifications are equivalent ?

	You can try proving the axioms in one specification from those in the
	other. 

4. How can I check whether one specification subsumes another,
   i.e., the first datatype can emulate the second ?

	Here I presume you are asking something more than half of item 3, i.e.,
	that you are asking how one goes about proving the correctness of an
	implementation of an abstract data type.  Again the problem boils down
	to defining the emulation and proving that it satisfies the axioms of
	the second datatype.  You should consult standard books on programming 
	by refinement, e.g., a book on VDM, for details.

5. Are there any tools that support working with algebraic 
   specification ?  How good are they ?  Prolog, Lisp ?

	Yes, there are several such tools.  Some simply provide a language for
	formalizing an algebraic specification.  Others provide support for
	reasoning about specifications.  These reasoning tools generally employ
	techniques based on equational term-rewriting and induction.  The
	quality of the tools is hard to quantify: some have better user
	interfaces than others, some are more efficient, ...  You would have to
	try them to see which best meets your needs.

	One tool is LP, the Larch Prover, which is available by anonymous ftp 
	from MIT, as described in the following	announcement.  We have paid a
	fair amount of attention to designing LP's user interface and to making
	it efficient.  Among the other tools that can be used to reason about
	algebraic specifications are the following term-rewriting systems.

	  System	Contact
	  ------	-------
	* Asspegique	cc@lri.lri.fr
	* RRL		hzhang@cs.uiowa.edu
	* OBJ3		obj3dist@csl.sri.com
	* REVEAL	siva@univ-orleans.fr
	* uUTRL		bylund@cs.umu.se


 LP, The Larch Prover
 --------------------
 Release 2.2, November 27, 1991

     LP [1] is an interactive proof-assistant for a subset of multisorted
first-order logic.  It is designed to work efficiently on large problems and to
be used by relatively naive users.  Among its current uses are analyzing formal
specifications [2], reasoning about concurrent algorithms and hardware designs
[4,5], and proving theorems in algebra [3].

     LP's design is based on the assumption that initial attempts to state
conjectures correctly, and then prove them, usually fail.  As a result, LP is
designed to carry out routine (and possibly lengthy) steps in a proof
automatically and to provide useful information about why proofs fail, if and
when they do.  LP is not designed to find difficult proofs automatically;
instead, LP makes it easy for users to employ standard techniques such as
proofs by cases, induction, and contradiction.

     LP allows users to axiomatize theories by equations (i.e., quantifier-free
formulas), operator theories (e.g., commutativity), deduction rules (equivalent
to universal-existential formulas), and induction rules.  LP automatically
orients most equations into terminating rewrite rules, which it then uses in
equational term-rewriting to simplify axioms and conjectures.  LP automatically
applies deduction rules to derive consequences from newly asserted, simplified,
or proved equations and rewrite rules.

LP can be obtained by anonymous ftp from larch.lcs.mit.edu (18.26.0.95)
You should use a dialog such as
     csh>>ftp larch.lcs.mit.edu
     Name: anonymous
     Password: <your name and location>
     ftp> cd pub/lp
     ftp> binary
     ftp> get lp2.2.lib.tar.Z
     ftp> get lp2.2.decmips.Z
     ftp> quit
to get the file lp2.2.lib.tar.Z (~420K), which contains documentation and a
runtime library for LP, together with one of the following compressed
executable versions of LP:
     lp2.2.decmips.Z	for DEC/MIPS 3100 or 5000 workstations (~1.1 meg)
     lp2.2.mips.Z	for MIPS workstations (~1.1 meg)
     lp2.2.sparc.Z	for Sun Sparcstations (~1.4 meg)
     lp2.2.sun3.Z	for Sun-3 workstations under Sun Unix 4.3 (~260K)
     lp2.2.vax.Z	for DEC VAX computers under Berkeley Unix 4.3 with NFS
			or a compatible version of Unix such as Ultrix (~260K)

     To run LP on some other machine (e.g., a Sony or Hewlett-Packard
workstation), or under some other operating system (e.g., Berkeley 4.2 Unix or
Berkeley 4.3 Unix without NFS), you should get the compressed tar file
lp2.2.code.tar.Z (~535K) containing source code, as well as lp2.2.lib.tar.Z,
and compile your own executables.

     To compile LP, you will need a CLU compiler and runtime system.  For VAX
and 68000 based architectures, these are available by anonymous ftp from
pion.lcs.mit.edu (18.26.0.64) in the directory pub/clu.  For other
architectures, such as the DEC/MIPS workstations and Sun Sparcstations, a
portable CLU compiler is available by anonymous ftp from mintaka.lcs.mit.edu
(18.26.0.36) in the directory pub/pclu.  If you use this implementation of CLU,
which translates CLU sources into C, you may also want to get the compressed
tar file lp2.2.c.tar.Z containing the C translations of the CLU sources
(getting these files saves the time required for retranslation).  See the file
INSTALLING in the distribution for information about compiling LP and about
overcoming installation problems.

     No license is required for using LP.  The file COPYRIGHT in the
distribution contains further information about using and redistributing LP.


References
----------

[1] S. J. Garland and J. V. Guttag.  A Guide to LP, The Larch Prover.  MIT 
    Laboratory for Computer Science, December 1991.  Also available from DEC 
    Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, as Report 
    82.  A PostScript file containing this report is part of the distribution.

[2] S. J. Garland, J. V. Guttag, and J. J. Horning. "Debugging Larch Shared
    Language specifications," IEEE Transactions on Software Engineering 16:9
    (September 1990), pp. 1044-1057.  Also available as DEC Systems Research 
    Center Report 60 (July 1990).

[3] U. Martin and M. Lai, "Some experiments with a completion theorem prover,"
    Journal of Symbolic Computation, to appear, 1991.

[4] J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning, "Using
    transformations and verification in circuit design," DEC Systems Research
    Center Report 78, September 1991.

[5] J. Staunstrup, S. J. Garland, and J. V. Guttag.  "Localized verification of
    circuit descriptions," Proc. Int. Workshop on Automatic Verification
    Methods for Finite State Systems, Grenoble, France, Lecture Notes in 
    Computer Science 407, Springer-Verlag, 1989, pp. 349-364.
---------------------------------------------------------------------------
Date: 26 Oct 1992 09:50:39 +0100
From: "Tilanus P.A.J." <P.A.J.Tilanus@research.ptt.nl>

Dear Lutz,

In comp.specification you write:

>1. How can I check whether my axioms really cover the functionality 
>   I have in mind ?  I know that this can not be done formally.

I wrote a paper for the 5th SDL Forum with the title
	How to get Complete ADT definitions/ - A Tutorial.
It might be relevant to this first question.
The proceedings of the 5th SDL Forum are published by North Holland in 1991;
the editor of the book is Rick Reed.  (I don't have the book on my desk, if
you need more information I can get it from our library.)

Success,

Paul Tilanus
P.A.J.Tilanus@research.ptt.nl
phone: +31 70 332 57 97
---------------------------------------------------------------------------
Date: Mon, 26 Oct 1992 10:33:16 GMT
From: Arie.van.Deursen@cwi.nl

|> 1. How can I check whether my axioms really cover the functionality 
|>    I have in mind ?  I know that this can not be done formally.
|> 
|> 2. How can I check whether I have redundant axioms ?
|> 
|> 3. How can I check whether two given specifications are equivalent ?
|> 
|> 4. How can I check whether one specification subsumes another,
|>    i.e., the first datatype can emulate the second ?
|> 
I have the feeling that you are posing some questions which are,
just like most interesting questions, undecidable in general.
As a practical guideline, I always try to distinguish the constructor
functions and defined functions first, and strive for sufficient-completeness
(who does not, anyway). The clarity thus gained helps when reasoning about the
specification.
Question 1: use tools (see question 5).
Question 2: If you suspect a particular axiom to be redundant, negate it, and
try to reach a contradiction. If you find it, the axiom was a logical 
consequence of the other axioms (hence, redundant) 
(detect it using resolution).


|> 5. Are there any tools that support working with algebraic 
|>    specification ?  How good are they ?  Prolog, Lisp ?
Yes there are. 
Here is our default information file for our system (Lisp, indeed).
I think you definitely need some automatic support to answer your 
first question (validation).

--------

The ASF+SDF Project

To allow for programming environments (integrated collections of tools)
that are both easy to obtain and provably correct, it is investigated
how tools can be generated from algebraic specifications of programming
languages.


Algebraic Specification using ASF+SDF

All specifications are algebraic specifications, using the ASF+SDF formalism.
The ASF+SDF formalism combines the elder "Algebraic Specification Formalism"
with the "Syntax Definition Formalism". By viewing signatures also as
grammars, concrete syntax can be used for terms (e.g., in the equations).
The formalism supports modularization, conditional equations (both 
positive and negative), and built-in associative lists.
The formalism is suited to provide specifications for arbitrary
abstract data types (traditional algebraic specification), as well as
definitions of any (formal) language (e.g. programming, query, text-processing,
specification, etc.).


The ASF+SDF Meta-environment

A system, called the ASF+SDF Meta-environment, has been built around the 
ASF+SDF formalism. It allows for rapid prototyping of ASF+SDF specifications.
>From the signature, parsers are geneated, and from the equations, term
rewriting systems are generated. Terms can be edited using syntax-directed
editors. It is possible to attach specified functionality to user-interface
events such as mouse-clicks, buttons, etc.
The ASF+SDF Meta-environment has an incremental implementation; if the
specification is changed the prototyped tools are adapted rather than
regenerated from scratch. This supports inter-active developing and testing
of specifications.
The system is still under development, but stable enough for external use.
A tape with the system is available.


Availability of Reports

There is an annotated bibliography list of abstracts of papers and 
publications of the ASF+SDF group. This abstract list can be obtained
by ftp to "ftp.cwi.nl", directory "pub/gipe". In this directory also
electronic versions of several reports can be found.


Some References:

@book{BHK89,
  editor      = {J.A. Bergstra and J. Heering and P. Klint},
  title       = {{A}lgebraic {S}pecification},
  series      = {ACM Press Frontier Series},
  publisher   = {The ACM Press in co-operation with Addison-Wesley},
  year        = {1989}}

@inproceedings{Kli91.meta,
   author = {P. Klint},
   booktitle = {Proceedings of the  METEOR workshop on Methods Based on
                Formal Specification},
   editor = {J.A. Bergstra and L.M.G. Feijs},
   pages = {105-124},
   publisher = {Springer-Verlag},
   series = {Lecture Notes in Computer Science},
   title = {A meta-environment for generating programming environments},
   volume = {490},
   year = {1991},
   institution = {Centrum voor Wiskunde en Informatica (CWI)},
   type = {Report {CS}-{R}9064}}

@article{HKR90,
  author      = {J. Heering and P. Klint and J. Rekers},
  title       = {{I}ncremental generation of parsers},
  journal     = {IEEE Transactions on Software Engineering},
  volume      = {16},
  number      = {12},
  pages       = {1344-1351},
  year        = {1990},
  note        = {Also in: {\it SIGPLAN Notices}, 24(7):179-191, 1989} }
---------------------------------------------------------------------------
Date: Tue, 27 Oct 92 08:41:06 +0100
From: Michael Mehlich <mehlich@informatik.uni-muenchen.de>

> 1. How can I check whether my axioms really cover the functionality 
>    I have in mind ?  I know that this can not be done formally.

When you have an "executable" specification it is possible to use  
prototyping methods like e.g. the RAP-system (developed in Passau).  
With such a system you can get ground substitutions for free  
variables which then satisfy conditional equations. The problem is,  
that your axioms already must be conditional equations. Hence, some  
development steps are necessary to perfrom the axioms.
Another way is to proof some properties which should be fulfilled by  
the specification. There are some (interactive, so called half  
automatic) proof systems you can use for it, e.g. Larch, Isabelle or  
TIP. A proof system, called KIV (developed in Karlsruhe), is just  
being adapted to algebraic specifications.

> 2. How can I check whether I have redundant axioms ?

I know only one way to do that. You must try to proof for each axiom  
if it can be derived from the other ones. When that is possible this  
axiom is really redundant.

> 3. How can I check whether two given specifications are equivalent ?

That is the next question in both directions.

> 4. How can I check whether one specification subsumes another,
>    i.e., the first datatype can emulate the second ?

One specification s is more special than another one t if all axioms  
of t follow from the axioms of s. (Then s is called a semantical  
refinement of t.) You only(?) have to proof that. But in practice  
other relations between specifications are also important.

> 5. Are there any tools that support working with algebraic 
>    specification ?  How good are they ?  Prolog, Lisp ?

I do not know any worth mentioning, but there may exist some.

Ich hoffe, Dir damit etwas geholfen zu haben

Ciao
  Michael
---------------------------------------------------------------------------