Consider a simple graph domain:

sig Graph {
   nodes : set Node,
   edges : set Edge,
}

sig Node {}

sig Edge {
   source : set Node,
   target : set Node
}

Suppose we want to write a function that for a given node n in a graph G
computes the set of all reachable nodes in G, i.e., n.*(~target.source)

We know how to define this function but there are several ways to declare it:

fun allTargets0[n:Node] : set Node
{ n.*(~source.target)  }

fun Graph::allTargets1[n:Node] : set Node
{ n.*(~source.target)  }

fun Graph::allTargets2[n:one this.nodes] : some this.nodes
{ n.*(~source.target)  }

fun Graph::allTargets3[n:this.nodes] : some this.nodes
{ n.*(~source.target)  }

Which of these contenders is preferable?

allTargets0 is the least preferable because it ignores the graph altogether.

allTargets1 is the simplest but it has properties that might be undesirable.

allTargets2 has a type signature that perhaps is the closest to our intent;
however, some of the type precision is ignored: allTargets2 is indistinguishable from allTargets3.

I suppose a similar analysis could be made which would result in concluding that the only specification that is correct w.r.t. our intent is allTargets0, i.e., the one that is least informative w.r.t. our intent.

See attached for some tests on this.



 

 

Attachment	Size
Contender.als (the web interface refuses *.als extensions)	1.93 KB