org.jmlspecs.samples.list.node2
Class DualLink

java.lang.Object
  org.jmlspecs.samples.list.node2.Link
      org.jmlspecs.samples.list.node2.DualLink

public class DualLink

extends Link

Class Specifications

protected invariant (this.node == null||this.node instanceof org.jmlspecs.samples.list.node2.TwoWayNode)&&this.node == this.dualNode; protected invariant this.node == this.dualNode; protected represents dualNode <- this.dualNode_; protected represents prevEntries <- this.prevEntriesMap(this);

Specifications inherited from class Link

protected represents node <- this.node_; protected represents entries <- entriesMap(this);

Specifications inherited from class Object

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

Model Field Summary
TwoWayNode	dualNode
JMLObjectSequence	prevEntries

 

Model fields inherited from class org.jmlspecs.samples.list.node2.Link

entries, node

 

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
protected  TwoWayNode	dualNode_

 

Fields inherited from class org.jmlspecs.samples.list.node2.Link

node_

 

Constructor Summary

DualLink()

DualLink(nullable TwoWayNode node)

 

Model Method Summary
protected  JMLObjectSequence	prevEntriesMap(nullable DualLink link)

 

Model methods inherited from class org.jmlspecs.samples.list.node2.Link

entriesMap

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
DualLink	getPrevious()

 

Methods inherited from class org.jmlspecs.samples.list.node2.Link

getEntry, getNext, toString

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

prevEntries

public JMLObjectSequence prevEntries

Specifications:
is in groups: entries
datagroup contains: dualNode

dualNode

public TwoWayNode dualNode

Specifications: nullable
is in groups: prevEntries node
datagroup contains: dualNode_

dualNode_

protected TwoWayNode dualNode_

Specifications: nullable
is in groups: dualNode

DualLink

public DualLink()

Specifications: (class)pure

public normal_behavior
assignable entries;
ensures this.node == null;

DualLink

public DualLink(nullable TwoWayNode node)

Specifications: (class)pure

public normal_behavior
assignable entries;
ensures this.dualNode == node;

prevEntriesMap

protected JMLObjectSequence prevEntriesMap(nullable DualLink link)

Specifications: pure

protected normal_behavior
requires link != null&&link.getEntry() != null;
ensures \result .equals(this.prevEntriesMap(link.getPrevious()).insertBack(link.getEntry()));

     also

requires link == null;
ensures \result .equals(new org.jmlspecs.models.JMLObjectSequence());

getPrevious

public DualLink getPrevious()

Specifications: nullable (class)pure

public normal_behavior
requires this.dualNode == null;
assignable \nothing;
ensures \result == null;

     also

public normal_behavior
requires this.dualNode != null;
assignable \nothing;
ensures \result .dualNode == this.dualNode.prevNode;