Name

Expression

Precondition

Semantics

Postcondition

Character assignment

X::assign(c1, c2)


Performs the assignment c1 = c2

X::eq(c1, c2) is true.

Character equality

X::eq(c1, c2)


Returns true if and only if c1 and c2 are equal.


Character comparison

X::lt(c1, c2)


Returns true if and only if c1 is less than c2. Note that
for any two value values c1 and c2, exactly one of
X::lt(c1, c2), X::lt(c2, c1), and X::eq(c1, c2) should be
true.


Range comparison

X::compare(p1, p2, n)

[p1, p1+n) and [p2, p2+n) are valid ranges.

Generalization of strncmp. Returns 0 if every element
in [p1, p1+n) is equal to the corresponding element
in [p2, p2+n), a negative value if there exists an element
in [p1, p1+n) less than the corresponding element in [p2, p2+n)
and all previous elements are equal, and a positive value
if there exists an element in [p1, p1+n) greater than the
corresponding element in [p2, p2+n) and all previous elements
are equal.


Length

X::length(p)


Generalization of strlen.
Returns the smallest nonnegative number n such that
X::eq(p+n, X::char_type()) is true. Behavior is undefined
if no such n exists.


Find

X::find(p, n, c)

[p, p+n) is a valid range.

Generalization of strchr. Returns the first pointer q
in [p, p+n) such that X::eq(*q, c) is true. Returns a
null pointer if no such pointer exists. (Note that this method
for indicating a failed search differs from that is
find.)


Move

X::move(s, p, n)

[p, p+n) and [s, s+n) are valid ranges (possibly overlapping).

Generalization of memmove. Copies values from the range
[p, p+n) to the range [s, s+n), and returns s.


Copy

X::copy(s, p, n)

[p, p+n) and [s, s+n) are valid ranges which do not overlap.

Generalization of memcpy. Copies values from the range
[p, p+n) to the range [s, s+n), and returns s.


Range assignment

X::assign(s, n, c)

[s, s+n) is a valid range.

Generalization of memset. Assigns the value c to each pointer
in the range [s, s+n), and returns s.


EOF value

X::eof()


Returns a value that can represent EOF.

X::eof() is distinct from every valid value of type
X::char_type. That is, there exists no value c
such that X::eq_int_type(X::to_int_type(c), X::eof()) is true.

Not EOF

X::not_eof(e)


Returns e if e represents a valid char_type value, and some
nonEOF value if e is X::eof().


Convert to value type

X::to_char_type(e)


Converts e to X's char type. If e is a representation of some
char_type value then it returns that value; if e is X::eof()
then the return value is unspecified.


Convert to int type

X::to_int_type(c)


Converts c to X's int type.

X::to_char_type(X::to_int_type(c)) is a null operation.

Equal int type values

X::eq_int_type(e1, e2)


Compares two int type values. If there exist values of type
X::char_type such that e1 is X::to_int_type(c1)) and
e2 is X::to_int_type(c2)), then X::eq_int_type(e1, e2) is
the same as X::eq(c1, c2). Otherwise, eq_int_type returns
true if e1 and e2 are both EOF and false if one of
e1 and e2 is EOF and the other is not.

