🚀 go-pugleaf

> I have been struggling with an algebraic spec for a couple of days and
> ...
> More specifically, I am trying to specify a tree that has the notion of
> a "current node", and operations to change the current node.  The ....
> Jeff Offutt
> Department of ISSE, George Mason University, Fairfax VA
> email: ofut@gmuvax2.gmu.edu
> phone: (703) 993-1654 (messages: 993-1640)

It has been shown that Majester's stack (sp?), which is a stack with 
a pointer to an arbitrary element (if memory serves), requires an infinite
set of algebraic axioms to specify.  

The practical point is that algebraic specs are very poor at
describing objects with state.  If you want to describe such an
object, use a model based spec language (such as Z).

-steve

********************************************************
* Steven Kearns            ....uunet!softrue!kearns    *
* Software Truth           softrue!kearns@uunet.uu.net *
********************************************************

In article <1992Dec31.000439.8884@gmuvax2.gmu.edu>, ofut@gmuvax2.gmu.edu
  (A. Jeff Offutt) writes:
> I have been struggling with an algebraic spec for a couple of days and
> am beginning to wonder if I am trying to do something that is
> impossible.  Intuitively, the feeling is similar to that of trying to
> describe a context free language using regular expressions.
> 
> Generally, are there _known_ fundamental limitations of algebraic
> specifications?  Has anyone studied the "classes" of ADTs that can be
> specified using various specification approaches?  If so, I would
> appreciate a reference (or a short synopsis, if possible).

I believe that there are, but the subject is out of my area of
competence.  However, what you are trying to do is indeed possible.

> More specifically, I am trying to specify a tree that has the notion of
> a "current node", and operations to change the current node.  The
> current node is a headache, mainly because I have different kinds of
> constructors -- some that modify the tree structure (adding/deleting
> nodes) and others that modify the current node.  My real problem,
> though, is with an operation that changes the current node to the
> root.
> 
> Does anyone konw offhand if that is possible ... and if it is, how?

The problem is that tree implementations usually severely restrict the
operations available, which makes formal manipulation of their
properties difficult.  One solution is to first define an auxiliary
tree type, which has nice mathematical properties but is not intended
for implementation. Then define the tree type you will actually use in
terms of the auxiliary type.

Here is one such auxiliary type.  The fundamental operation is  t.p  ,
which represents the subtree of  t  obtained by following the path  p 
from the root.  If  p  is empty, then  t.p  is just  t  .  Thus if we
are talking about binary trees with left and right branches, we would
say something like  t.<left,right>  instead of  right(left(t))  .

Paths are just strings of directions.  In following,  p^q  is  p 
followed by  q  ;  <>  is the empty path;  <j>  is the path whose first
and only element is  j  ; and  p`n  is  p  with its last  n  elements
removed.

Then given types

  Index = {left,right}         -- or whatever
  Path = string of Index
  Value =  < some arbitrary type >

we specify the auxTree type as follows.  (The  PRE  clauses specify when
a function application is defined.)

for   t, t1: auxTree   p, p1: Path   j: Index   v: Value 

(binary operator) . : auxTree x Path -> auxTree
   PRE(t.p) = p in dom(t)
dom: auxTree -> set of Path
   PRE(dom(t)) = true
singleton: Value -> auxTree
   PRE(singleton(v)) = true
val: auxTree -> Value
   PRE(val(t)) = true
add: auxTree x Path x auxTree -> auxTree
   PRE(add(t,<>,v)) = false
   PRE(add(t,p^<j>,v)) = p in dom(t) & not(p^<j> in dom(t))
remove: auxTree x Path -> auxTree
   PRE(remove(t,<>)) = false
   PRE(remove(t,p^<j>)) = p^<j> in dom(t)

t.<> = t
t.(p^<j>) = (t.p).<j>
dom(singleton(v)) = <>
dom(add(t,p,v)) = dom(t) union {p}
dom(remove(t,p^<j>)) = dom(t) - {p^<j>}
val(singleton(v)) = v
val(add(t,p,t1)) = val(t)
add(t,p^<j>,t1).p1 = if p1=p^<j> -> t1 else t.p1 fi
remove(t,p^<j>).p1 = t.p1		-- if it's legal!


Give the auxTree type, we can specify a more concrete uTree type as a
pair consisting of an auxTree and a path pointing to the current node in
the auxTree.

The starred functions below are auxiliary functions, and need not be
implemented.

for  v, j  as above and   u, u1: uTree

*tree: uTree -> Tree
    PRE(tree(u)) = true
*current: uTree -> Path
    PRE(current(u)) = true
 usingleton: Value -> uTree
    PRE(usingleton(v)) = true
 curval: uTree -> Value
    PRE(curval(u)) = true
 go: uTree x Index -> uTree
    PRE(go(u,j)) = current(u)^<j> in dom(tree(u))
 goroot: uTree -> uTree
    PRE(goroot(u)) = true
 addcur: uTree x Index x uTree -> uTree
    PRE(addcur(u,j,u1)) = 
       current(u) in dom(tree(u)) & not(current(u)^<j> in dom(tree(u))
 trim: uTree -> uTree
    PRE(trim(u)) = current(u) != <>

tree(usingleton(v)) = singleton(v)
current(usingleton(v)) = <>

curval(u) = val(tree(u).current(u))

tree(go(u,j)) = tree(u)
current(go(u,j)) = current(u)^<j>

tree(goroot(u)) = tree(u)
current(goroot(u)) = <>

tree(addcur(u,j,u1)) = add(tree(u),current(u)^<j>,tree(u1))
current(addcur(u,j,u1)) = current(u)^<j>

tree(trim(u)) = remove(tree(u),current(u))
current(trim(u)) = current(u)`1             -- current(u) with its
                                            -- last element removed


> If you are interested and can offer more help, we can talk via email
> about the specifics of the data structure I am working with.
> -- 
> Jeff Offutt
> Department of ISSE, George Mason University, Fairfax VA
> email: ofut@gmuvax2.gmu.edu
> phone: (703) 993-1654 (messages: 993-1640)

Antediluvian newsbreak:           |  J. E. Fritz    (fritz@ruby.vcu.edu)
  Scientists discover 4th prime.  |  VCU and I don't talk _to_ each other,
  Proof at eleven.                |  let alone for each other.

In article <36.UUL1.3#8618@softrue.UUCP>, kearns@softrue.UUCP (Steven Kearns)
writes:
>> I have been struggling with an algebraic spec for a couple of days and
>> ...
>> More specifically, I am trying to specify a tree that has the notion of
>> a "current node", and operations to change the current node.  The ....
>> Jeff Offutt
>> Department of ISSE, George Mason University, Fairfax VA
>> email: ofut@gmuvax2.gmu.edu
>> phone: (703) 993-1654 (messages: 993-1640)
[...]
> 
> It has been shown that Majester's stack (sp?), which is a stack with 
> a pointer to an arbitrary element (if memory serves), requires an infinite
> set of algebraic axioms to specify.  

Only if you disallow auxiliary functions (functions not intended to be
implemented).

> The practical point is that algebraic specs are very poor at
> describing objects with state.  If you want to describe such an
> object, use a model based spec language (such as Z).

Could you give us a short example, say of the extended stack you mention
above?

> -steve
> 
> ********************************************************
> * Steven Kearns            ....uunet!softrue!kearns    *
> * Software Truth           softrue!kearns@uunet.uu.net *
> ********************************************************

Antediluvian newsbreak:           |  J. E. Fritz    (fritz@ruby.vcu.edu)
  Scientists discover 4th prime;  |  VCU and I don't talk _to_ each other,
  proof at eleven.                |  let alone for each other.

In article <1992Dec31.000439.8884@gmuvax2.gmu.edu>, ofut@gmuvax2.gmu.edu (A. Jeff Offutt) writes:
> Generally, are there _known_ fundamental limitations of algebraic
> specifications?  Has anyone studied the "classes" of ADTs that can be
> specified using various specification approaches?  If so, I would
> appreciate a reference (or a short synopsis, if possible).

Some standard references on this topic are:

   J. Thatcher, E. Wagner and J. Wright.  Data type specification:
   parameterization and the power of specification techniques.  ACM Trans. on
   Programming Languages and Systems 4, 711-773 (1982).

   J. Bergstra, M. Broy, J. Tucker and M. Wirsing.  On the power of algebraic
   specifications.  Proc. 1981 Symp. on Mathematical Foundations of Computer
   Science.  Springer LNCS 118, 193-204 (1981).

   J. Bergstra and J. Tucker.  Initial and final algebra semantics: two
   characterization theorems.  SIAM Journal on Computing 12(2), 366-387 (1983).

   J. Bergstra and J. Tucker.  Algebraic specifications of computable and
   semicomputable data types.  Theoretical Computer Science 50, 137-181 (1987).

Briefly, there are different approaches to algebraic specification and
the expressive power of a particular approach depends on whether or not it
offers certain features.  One of the simplest approaches and the most classical
is the so-called "initial algebra approach" via finite lists of equational
axioms as described in:

   H. Ehrig and B. Mahr.  Fundamentals of Algebraic Specification 1. Equations
   and Initial Semantics.  EATCS Monographs on Theoretical Computer Science.
   Springer (1985).

This approach is not powerful enough to specify all recursive data structures
(using "recursive" here in its recursion-theoretic sense).  Allowing hidden
sorts and hidden functions makes this approach powerful enough to describe
exactly all the semicomputable algebras.  Adding so-called "data constraints"
or "hierarchy constraints" (or using a specification language in which the
specification of new types of data cannot side-effect the interpretation of
existing types, e.g. ASL) makes it possible to code universal and existential
quantifiers over the natural numbers and so adds considerable expressive power,
enough to allow the specification of any algebra you are likely to want (for
the details of that vague statement see [BBTW81]).

A paper which explains some of the above and discusses its relevance to
completeness of systems for proving theorems about specifications is:

   D. MacQueen and D. Sannella.  Completeness of proof systems for equational
   specifications.  IEEE Trans. on Software Engineering SE-11(5), 454-461
   (1985).

Of course, all of these expressiveness results are obtained via codings which,
if used in practice, would make specifications difficult (if not impossible)
to read.  Whether or not a particular data type can be *conveniently* specified
is a different question.


Don Sannella
University of Edinburgh