Class KindVector

java.lang.Object
es.ucm.maude.bindings.KindVector
public class KindVector extends Object
Internal Maude vector.

  • Constructor Summary

    Constructors
    Constructor
    Description
    KindVector()
    Construct a vector.

    KindVector(long length)
    Construct a vector.

  • Method Summary

    Modifier and Type
    Method
    Description
    void
    append(Kind value)
    Append a new element to the vector.
    long
    capacity()
    Reserved capacity of the vector.
    void
    clear()
    Set the vector length to zero.
    void
    delete()
     
    boolean
    empty()
    Is the vector empty?
    Kind
    get(long n)
    Get a vector position value.

    void
    resize(long new_size)
    Resize the vector.

    void
    set(long n, Kind value)
    Set a vector position value.

    long
    size()
    Size of the vector.
    void
    swap(KindVector other)
    Swap this vector's contents with another.

    Methods inherited from class java.lang.Object

    equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • KindVector

      public KindVector(long length)
      Construct a vector.

      Parameters:
      length - The initial length.

    • KindVector

      public KindVector()
      Construct a vector.

  • Method Details

    • delete

      public void delete()

    • empty

      public boolean empty()
      Is the vector empty?

    • size

      public long size()
      Size of the vector.

    • capacity

      public long capacity()
      Reserved capacity of the vector.

    • swap

      public void swap(KindVector other)
      Swap this vector's contents with another.

      Parameters:
      other - The other vector.

    • get

      public Kind get(long n)
      Get a vector position value.

      Parameters:
      n - Vector position from zero.

    • set

      public void set(long n, Kind value)
      Set a vector position value.

      Parameters:
      n - Vector position from zero.
      value - Value to be set.

    • append

      public void append(Kind value)
      Append a new element to the vector.

    • clear

      public void clear()
      Set the vector length to zero.

    • resize

      public void resize(long new_size)
      Resize the vector.

      Parameters:
      new_size - New size.