org.jmlspecs.samples.list.node2
Class Link

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

Direct Known Subclasses:

DualLink

public class Link

extends Object

Class Specifications

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
JMLObjectSequence	entries
OneWayNode	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  OneWayNode	node_

 

Constructor Summary

Link()

Link(nullable OneWayNode node)

 

Model Method Summary
static JMLObjectSequence	entriesMap(Link link)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	getEntry()
Link	getNext()
String	toString()

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

entries

public JMLObjectSequence entries

Specifications:
datagroup contains: node org.jmlspecs.samples.list.node2.DualLink.prevEntries

node

public OneWayNode node

Specifications: nullable
is in groups: entries
datagroup contains: node_ org.jmlspecs.samples.list.node2.DualLink.dualNode

node_

protected OneWayNode node_

Specifications: nullable
is in groups: node

Link

public Link()

Specifications: (class)pure

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

Link

public Link(nullable OneWayNode node)

Specifications: (class)pure

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

entriesMap

public static JMLObjectSequence entriesMap(Link link)

Specifications: pure

protected normal_behavior
requires link.node != null;
ensures \result .equals(entriesMap(link.getNext()).insertFront(link.getEntry()));

     also

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

getEntry

public Object getEntry()

Specifications: nullable (class)pure

public normal_behavior
assignable \nothing;
ensures \result == this.node.getEntry();

getNext

public Link getNext()

Specifications: nullable (class)pure

public normal_behavior
assignable \nothing;
ensures \result .node == this.node.nextNode;

toString

public String toString()

Overrides:

toString in class Object

Specifications: (class)pure

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;