Java Doc for JMLObjectSequence.java in » Testing » KeY » org » jmlspecs » models » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation

1.	6.0 JDK Core
2.	6.0 JDK Modules
3.	6.0 JDK Modules com.sun
4.	6.0 JDK Modules com.sun.java
5.	6.0 JDK Modules sun
6.	6.0 JDK Platform
7.	Ajax
8.	Apache Harmony Java SE
9.	Aspect oriented
10.	Authentication Authorization
11.	Blogger System
12.	Build
13.	Byte Code
14.	Cache
15.	Chart
16.	Chat
17.	Code Analyzer
18.	Collaboration
19.	Content Management System
20.	Database Client
21.	Database DBMS
22.	Database JDBC Connection Pool
23.	Database ORM
24.	Development
25.	EJB Server geronimo
26.	EJB Server GlassFish
27.	EJB Server JBoss 4.2.1
28.	EJB Server resin 3.1.5
29.	ERP CRM Financial
30.	ESB
31.	Forum
32.	GIS
33.	Graphic Library
34.	Groupware
35.	HTML Parser
36.	IDE
37.	IDE Eclipse
38.	IDE Netbeans
39.	Installer
40.	Internationalization Localization
41.	Inversion of Control
42.	Issue Tracking
43.	J2EE
44.	JBoss
45.	JMS
46.	JMX
47.	Library
48.	Mail Clients
49.	Net
50.	Parser
51.	PDF
52.	Portal
53.	Profiler
54.	Project Management
55.	Report
56.	RSS RDF
57.	Rule Engine
58.	Science
59.	Scripting
60.	Search Engine
61.	Security
62.	Sevlet Container
63.	Source Control
64.	Swing Library
65.	Template Engine
66.	Test Coverage
67.	Testing
68.	UML
69.	Web Crawler
70.	Web Framework
71.	Web Mail
72.	Web Server
73.	Web Services
74.	Web Services apache cxf 2.0.1
75.	Web Services AXIS2
76.	Wiki Engine
77.	Workflow Engines
78.	XML
79.	XML UI

Java

Java Tutorial

Illustrator Tutorials

GIMP Tutorials

C# / C Sharp

C# / CSharp Tutorial

C# / CSharp Open Source

SQL Server / T-SQL Tutorial

Oracle PL / SQL

Oracle PL/SQL Tutorial

Flash / Flex / ActionScript

VBA / Excel / Access / Word

XML

XML Tutorial

Microsoft Office PowerPoint 2007 Tutorial

Microsoft Office Excel 2007 Tutorial

Microsoft Office Word 2007 Tutorial

Java Source Code / Java Documentation » Testing » KeY » org.jmlspecs.models

Source Cross Reference

Class Diagram

Java Document (Java Doc)

java.lang .Object

org.jmlspecs.models .JMLObjectSequence

JMLObjectSequence
public class JMLObjectSequence implements JMLCollection(Code)
	Sequences of objects. This type uses "==" to compare elements, and does not clone elements that are passed into and returned from the sequence's methods. The informal model for a JMLObjectSequence is a finite mathematical sequence of elements (of type Object ). In some examples, we will write <a,b,c> for a mathematical sequence of length 3, containing elements a, b, and c. Elements of sequences are "indexed" from 0, so the length of a sequence is always 1 more than the index of the last element in the sequence. version: $Revision: 1.3 $ author: Gary T. Leavens author: Albert L. Baker See Also: JMLCollection See Also: JMLType See Also: JMLValueSequence See Also: JMLObjectSequenceEnumerator

Field Summary
final public static JMLObjectSequence	EMPTY The empty JMLObjectSequence.
final protected BigInteger	_length
final protected JMLListObjectNode	theSeq An equational specification of the properties of sequences.

Constructor Summary
public	JMLObjectSequence()
public	JMLObjectSequence(Object e)
protected	JMLObjectSequence(JMLListObjectNode ls, int len) Initialize this sequence based on the given representation.

Method Summary
public Object	clone() Return a clone of this object.
public JMLObjectSequence	concat(JMLObjectSequence s2)
public boolean	containsAll(java.util.Collection c)
public static JMLObjectSequence	convertFrom(Object[] a) Return the sequence containing all the elements in the given array in the same order as the elements appear in the array.
public static JMLObjectSequence	convertFrom(Object[] a, int size) Return the sequence containing the first 'size' elements in the given array in the same order as the elements appear in the array.
public static JMLObjectSequence	convertFrom(java.util.Collection c) Return the sequence containing all the object in the given collection in the same order as the elements appear in the collection.
public static JMLObjectSequence	convertFrom(JMLCollection c) Return the sequence containing all the object in the given JMLCollection in the same order as the elements appear in the collection.
public int	count(Object item)
public JMLObjectSequenceEnumerator	elements()
public boolean	equals(Object obj) Test whether this object's value is equal to the given argument.
public Object	first()
public Object	get(int i) Return the element at the given zero-based index; a synonym for JMLObjectSequence.itemAt .
public boolean	has(Object elem)
public int	hashCode() Return a hash code for this object.
public JMLObjectSequence	header()
public int	indexOf(Object item)
public JMLObjectSequence	insertAfterIndex(int afterThisOne, Object item)
public JMLObjectSequence	insertBack(Object item)
public JMLObjectSequence	insertBeforeIndex(int beforeThisOne, Object item)
public JMLObjectSequence	insertFront(Object item)
public int	int_length()
public int	int_size()
public boolean	isDeletionFrom(JMLObjectSequence s2, Object elem)
public boolean	isEmpty() Tells whether this sequence is empty.
public boolean	isInsertionInto(JMLObjectSequence s2, Object elem)
public boolean	isPrefix(JMLObjectSequence s2)
public boolean	isProperPrefix(JMLObjectSequence s2)
public boolean	isProperSubsequence(JMLObjectSequence s2)
public boolean	isProperSuffix(JMLObjectSequence s2)
public boolean	isProperSupersequence(JMLObjectSequence s2)
public boolean	isSubsequence(JMLObjectSequence s2)
public boolean	isSuffix(JMLObjectSequence s2)
public boolean	isSupersequence(JMLObjectSequence s2)
public Object	itemAt(int i) Return the element at the given zero-based index.
public JMLIterator	iterator()
public Object	last()
public JMLObjectSequence	prefix(int n) Return a sequence containing the first n elements in this sequence.
public JMLObjectSequence	removeItemAt(int index)
public JMLObjectSequence	removePrefix(int n)
public JMLObjectSequence	replaceItemAt(int index, Object item)
public JMLObjectSequence	reverse()
public static JMLObjectSequence	singleton(Object e) Return the singleton sequence containing the given element.
public JMLObjectSequence	subsequence(int from, int to)
public Object[]	toArray()
public JMLObjectBag	toBag()
public JMLObjectSet	toSet()
public String	toString()
public JMLObjectSequence	trailer()

Field Detail

EMPTY
final public static JMLObjectSequence EMPTY(Code)
	The empty JMLObjectSequence. See Also: JMLObjectSequence.JMLObjectSequence()

_length
final protected BigInteger _length(Code)

theSeq
final protected JMLListObjectNode theSeq(Code)
	An equational specification of the properties of sequences.

Constructor Detail

JMLObjectSequence
public JMLObjectSequence()(Code)

JMLObjectSequence
public JMLObjectSequence(Object e)(Code)

JMLObjectSequence
protected JMLObjectSequence(JMLListObjectNode ls, int len)(Code)
	Initialize this sequence based on the given representation.

Method Detail

clone
public Object clone()(Code)
	Return a clone of this object. This method does not clone the elements of the sequence.

concat
public JMLObjectSequence concat(JMLObjectSequence s2)(Code)

containsAll
public boolean containsAll(java.util.Collection c)(Code)

convertFrom
public static JMLObjectSequence convertFrom(Object[] a)(Code)
	Return the sequence containing all the elements in the given array in the same order as the elements appear in the array.

convertFrom
public static JMLObjectSequence convertFrom(Object[] a, int size)(Code)
	Return the sequence containing the first 'size' elements in the given array in the same order as the elements appear in the array.

convertFrom
public static JMLObjectSequence convertFrom(java.util.Collection c) throws ClassCastException(Code)
	Return the sequence containing all the object in the given collection in the same order as the elements appear in the collection. throws: ClassCastException - if some element in c is not an instance of Object. See Also: JMLObjectSequence.containsAll(java.util.Collection)

convertFrom
public static JMLObjectSequence convertFrom(JMLCollection c) throws ClassCastException(Code)
	Return the sequence containing all the object in the given JMLCollection in the same order as the elements appear in the collection. throws: ClassCastException - if some element in c is not an instance of Object.

count
public int count(Object item)(Code)

elements
public JMLObjectSequenceEnumerator elements()(Code)

equals
public boolean equals(Object obj)(Code)
	Test whether this object's value is equal to the given argument. See Also: JMLObjectSequence.isSuffix See Also: JMLObjectSequence.int_size()

first
public Object first() throws JMLSequenceException(Code)

get
public Object get(int i) throws IndexOutOfBoundsException(Code)
	Return the element at the given zero-based index; a synonym for JMLObjectSequence.itemAt . Parameters: i - the zero-based index into the sequence. exception: IndexOutOfBoundsException - if the index i is out of range. See Also: JMLObjectSequence.itemAt(int)

has
public boolean has(Object elem)(Code)

hashCode
public int hashCode()(Code)
	Return a hash code for this object.

header
public JMLObjectSequence header() throws JMLSequenceException(Code)

indexOf
public int indexOf(Object item) throws JMLSequenceException(Code)

insertAfterIndex
public JMLObjectSequence insertAfterIndex(int afterThisOne, Object item) throws JMLSequenceException, IllegalStateException(Code)

insertBack
public JMLObjectSequence insertBack(Object item) throws IllegalStateException(Code)

insertBeforeIndex
public JMLObjectSequence insertBeforeIndex(int beforeThisOne, Object item) throws JMLSequenceException, IllegalStateException(Code)

insertFront
public JMLObjectSequence insertFront(Object item) throws IllegalStateException(Code)

int_length
public int int_length()(Code)

int_size
public int int_size()(Code)

isDeletionFrom
public boolean isDeletionFrom(JMLObjectSequence s2, Object elem)(Code)

isEmpty
public boolean isEmpty()(Code)
	Tells whether this sequence is empty. See Also: JMLObjectSequence.int_size() See Also: JMLObjectSequence.int_length()

isInsertionInto
public boolean isInsertionInto(JMLObjectSequence s2, Object elem)(Code)

isPrefix
public boolean isPrefix(JMLObjectSequence s2)(Code)

isProperPrefix
public boolean isProperPrefix(JMLObjectSequence s2)(Code)

isProperSubsequence
public boolean isProperSubsequence(JMLObjectSequence s2)(Code)

isProperSuffix
public boolean isProperSuffix(JMLObjectSequence s2)(Code)

isProperSupersequence
public boolean isProperSupersequence(JMLObjectSequence s2)(Code)

isSubsequence
public boolean isSubsequence(JMLObjectSequence s2)(Code)

isSuffix
public boolean isSuffix(JMLObjectSequence s2)(Code)

isSupersequence
public boolean isSupersequence(JMLObjectSequence s2)(Code)

itemAt
public Object itemAt(int i) throws JMLSequenceException(Code)
	Return the element at the given zero-based index. Parameters: i - the zero-based index into the sequence. exception: JMLSequenceException - if the index i is out of range. See Also: JMLObjectSequence.get(int) See Also: JMLObjectSequence.has(Object) See Also: JMLObjectSequence.count(Object) See Also: #itemAt(\bigint)

iterator
public JMLIterator iterator()(Code)

last
public Object last() throws JMLSequenceException(Code)

prefix
public JMLObjectSequence prefix(int n) throws JMLSequenceException(Code)
	Return a sequence containing the first n elements in this sequence. Parameters: n - the number of elements in the result. exception: JMLSequenceException - if n is negative or greater thanthe length of the sequence. See Also: JMLObjectSequence.trailer See Also: JMLObjectSequence.removePrefix See Also: JMLObjectSequence.subsequence

removeItemAt
public JMLObjectSequence removeItemAt(int index) throws JMLSequenceException(Code)

removePrefix
public JMLObjectSequence removePrefix(int n) throws JMLSequenceException(Code)

replaceItemAt
public JMLObjectSequence replaceItemAt(int index, Object item) throws JMLSequenceException(Code)

reverse
public JMLObjectSequence reverse()(Code)

singleton
public static JMLObjectSequence singleton(Object e)(Code)
	Return the singleton sequence containing the given element. See Also: JMLObjectSequence.JMLObjectSequence(Object)

subsequence
public JMLObjectSequence subsequence(int from, int to) throws JMLSequenceException(Code)

toArray
public Object[] toArray()(Code)

toBag
public JMLObjectBag toBag()(Code)

toSet
public JMLObjectSet toSet()(Code)

toString
public String toString()(Code)

trailer
public JMLObjectSequence trailer() throws JMLSequenceException(Code)

Methods inherited from java.lang.Object

protected Object clone() throws CloneNotSupportedException(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
protected void finalize() throws Throwable(Code)(Java Doc)
final native public Class getClass()(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
final public void notify() throws IllegalMonitorStateException(Code)(Java Doc)
final public void notifyAll() throws IllegalMonitorStateException(Code)(Java Doc)
public String toString()(Code)(Java Doc)
final public void wait() throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms, int ns) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)

www.java2java.com | Contact Us

All other trademarks are property of their respective owners.