org.jmlspecs.samples.digraph
Class Digraph

java.lang.Object
  org.jmlspecs.samples.digraph.Digraph

Direct Known Subclasses:

TransposableDigraph

public abstract class Digraph

extends Object

Directed graphs.

Author:

Katie Becker, Gary T. Leavens

Class Specifications

private invariant_redundantly this.nodeSet != null; private invariant ( \forall java.lang.Object e; this.nodeSet.contains(e); e != null&&e instanceof org.jmlspecs.samples.digraph.NodeType); private invariant_redundantly this.arcSet != null; private invariant ( \forall java.lang.Object e; this.arcSet.contains(e); e != null&&e instanceof org.jmlspecs.samples.digraph.Arc); public invariant_redundantly this.nodes != null; public invariant ( \forall org.jmlspecs.models.JMLType n; this.nodes.has(n); n instanceof org.jmlspecs.samples.digraph.NodeType); public invariant_redundantly this.arcs != null; public invariant ( \forall org.jmlspecs.models.JMLType a; this.arcs.has(a); a instanceof org.jmlspecs.samples.digraph.ArcType); public invariant ( \forall org.jmlspecs.samples.digraph.ArcType a; this.arcs.has(a); this.nodes.has(a.from)&&this.nodes.has(a.to)); private represents nodes <- org.jmlspecs.models.JMLValueSet.convertFrom(this.nodeSet); private represents arcs <- this.arcAbstractValue(this.arcSet);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
JMLValueSet	arcs
JMLValueSet	nodes

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] protected  HashSet	arcSet
[spec_public] protected  HashSet	nodeSet

 

Constructor Summary

Digraph()

 

Model Method Summary
private  JMLValueSet	arcAbstractValue(HashSet arcs)
JMLValueSet	OneMoreStep(JMLValueSet nodeSet)
JMLValueSet	reachSet(JMLValueSet nodeSet)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	addArc(NodeType inFrom, NodeType inTo)
void	addNode(NodeType n)
boolean	isAPath(NodeType start, NodeType end)
boolean	isArc(NodeType inFrom, NodeType inTo)
boolean	isNode(NodeType n)
protected  HashSet	reachSet(NodeType start)
void	removeArc(NodeType inFrom, NodeType inTo)
void	removeNode(NodeType n)
String	toString()
boolean	unconnected(NodeType n)

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Model Field Detail

nodes

public JMLValueSet nodes

Specifications:
datagroup contains: nodeSet nodeSet.theSet

arcs

public JMLValueSet arcs

Specifications:
datagroup contains: arcSet arcSet.theSet

nodeSet

protected HashSet nodeSet

Specifications: spec_public
is in groups: nodes
maps nodeSet.theSet \into nodes

arcSet

protected HashSet arcSet

Specifications: spec_public
is in groups: arcs
maps arcSet.theSet \into arcs

Digraph

public Digraph()

Specifications:

public normal_behavior
assignable nodes, arcs;
ensures this.nodes.isEmpty()&&this.arcs.isEmpty();

arcAbstractValue

private JMLValueSet arcAbstractValue(HashSet arcs)

Specifications: pure

reachSet

public JMLValueSet reachSet(JMLValueSet nodeSet)

Specifications: pure

public normal_behavior
requires_redundantly nodeSet != null;
requires ( \forall org.jmlspecs.models.JMLType o; nodeSet.has(o); o instanceof org.jmlspecs.samples.digraph.NodeType&&this.nodes.has(o));

{|

assignable \nothing;

also

requires nodeSet.equals(this.OneMoreStep(nodeSet));
ensures \result != null&&\result .equals(nodeSet);

also

requires !nodeSet.equals(this.OneMoreStep(nodeSet));
ensures \result != null&&\result .equals(this.reachSet(this.OneMoreStep(nodeSet)));

|}

OneMoreStep

public JMLValueSet OneMoreStep(JMLValueSet nodeSet)

Specifications: pure

public normal_behavior
requires_redundantly nodeSet != null;
requires ( \forall org.jmlspecs.models.JMLType o; nodeSet.has(o); o instanceof org.jmlspecs.samples.digraph.NodeType&&this.nodes.has(o));
assignable \nothing;
ensures_redundantly \result != null;
ensures \result .equals(nodeSet.union( new org.jmlspecs.models.JMLValueSet { org.jmlspecs.samples.digraph.NodeType n | this.nodes.has(n) && ( \exists org.jmlspecs.samples.digraph.ArcType a; a != null&&this.arcs.has(a); nodeSet.has(a.from)&&n.equals(a.to)) }));

addNode

public void addNode(NodeType n)

Specifications:

public normal_behavior
requires_redundantly n != null;
assignable nodes;
ensures this.nodes.equals(\old(this.nodes.insert(n)));

removeNode

public void removeNode(NodeType n)

Specifications:

public normal_behavior
requires this.unconnected(n);
assignable nodes;
ensures this.nodes.equals(\old(this.nodes.remove(n)));

addArc

public void addArc(NodeType inFrom,
                   NodeType inTo)

Specifications:

public normal_behavior
requires_redundantly inFrom != null&&inTo != null;
requires this.nodes.has(inFrom)&&this.nodes.has(inTo);
assignable arcs;
ensures this.arcs.equals(\old(this.arcs).insert(new org.jmlspecs.samples.digraph.ArcType(inFrom, inTo)));

removeArc

public void removeArc(NodeType inFrom,
                      NodeType inTo)

Specifications:

public normal_behavior
requires_redundantly inFrom != null&&inTo != null;
requires this.nodes.has(inFrom)&&this.nodes.has(inTo);
assignable arcs;
ensures this.arcs.equals(\old(this.arcs).remove(new org.jmlspecs.samples.digraph.ArcType(inFrom, inTo)));

isNode

public boolean isNode(NodeType n)

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.nodes.has(n);

     also

public normal_behavior
ensures \result == this.nodeSet.contains(n);

isArc

public boolean isArc(NodeType inFrom,
                     NodeType inTo)

Specifications: pure

public normal_behavior
requires_redundantly inFrom != null&&inTo != null;
ensures \result == this.arcs.has(new org.jmlspecs.samples.digraph.ArcType(inFrom, inTo));

isAPath

public boolean isAPath(NodeType start,
                       NodeType end)

Specifications: pure

public normal_behavior
requires this.nodes.has(start)&&this.nodes.has(end);
assignable \nothing;
ensures \result == this.reachSet(new org.jmlspecs.models.JMLValueSet(start)).has(end);

reachSet

protected HashSet reachSet(NodeType start)

Specifications: pure

toString

public String toString()

Overrides:

toString in class Object

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;

unconnected

public boolean unconnected(NodeType n)

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result <==> !( \exists org.jmlspecs.samples.digraph.ArcType a; this.arcs.has(a); a.from.equals(n)||a.to.equals(n));