🚀 go-pugleaf

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.