using:standard_lib

Standard Library

  • Nat, Int, Real
  • +, , , /, ^
  • <=, >=, >, <
  • ..
  • Infinity

The Sequences module defines operations on finite sequences. We represent a finite sequence as a tuple, so the sequence of three numbers 3, 2, 1 is the triple <<3, 2, 1>>. The Sequences module defines the following operators on sequences:

  • s \o t: The sequence obtained by concatenating the sequences s and t.
    • Example: <<3, 7>> \o <<3>> is equal to <<3, 7, 3>>.
  • Head(s): The first element of the sequence s.
    • Example: Head(<<3,2,1>>) is equal to 3
  • SelectSeq(s, Test): The subsequence of s consisting of the elements s[i] such that Test(s[i]) equals true.
    • Example:
      PosSubSeq(s) == LET IsPos(n) == n > 0
                      in SelectSeq(s, IsPos)

      defines PosSubSeq(<<0, 3, −2, 5>>) to be equal to <<3, 5>>

  • SubSeq(s, m, n): The subsequence <<s[m], s[m + 1], . . . , s[n]>> consisting of the mth through nth elements of s. It is undefined if m < 1 or n > Len(s), except that it equals the empty sequence if m > n.
  • Append(s, e): The sequence obtained by appending element e to the tail of sequence s.
    • Example: Append(<<3, 7>>, 3) equals <<3, 7, 3>>.
  • Len(s): The length of sequence s.
    • Example: Len(<<1,2,3>>) is equal to 3.
  • Seq(S): The set of all sequences of elements of the set S .
    • Example: Seq({3,7}) is equal to <<3, 7>>.
  • Tail(s): The tail of sequence s, which consists of s with its head element removed.
    • Example: Tail(<<3, 7>>) equals <<7>>.
  • IsFiniteSet(s): A set is finite iff there is a finite sequence containing all its elements.
    • Example: IsFiniteSet({1,2,3}) is equal to TRUE
  • Cardinality(s): The number of elements in the set s. It's only defined for finite sets.
    • Example: Cardinality({1,2}) is equal to 2.
  • (+), (-)
  • BagIn
  • CopiesIn
  • SubBag
  • BagOfAll
  • EmptyBag
  • \sqsubseteq
  • BagToSet
  • IsABag
  • BagCardinality
  • BagUnion
  • SetToBag
  • RTBound
  • RTnow
  • now
  • :>, @@
  • Print
  • Assert
  • JavaTime
  • Permutations
  • SortSeq
  • using/standard_lib.txt
  • Last modified: 2024/10/10 16:42
  • by fponzi