Next / Previous / Contents / Shipman's homepage

5.6. Intended function examples

To illustrate some typical intended functions, here are some examples from Python and its libraries. In each example, the wording before the code fragment is taken from the official Python documentation.

any(I)

Return True if any element of the iterable I is true. If the iterable is empty, return False.

    # [ i is an iterable ->
    #     if there exists any element k in i such that bool(k) is True ->
    #       test  :=  True
    #     else ->
    #       test  :=  False ]
    test = any(i)

The precondition stipulates that the argument must be an iterable. This intended function covers the case that I is empty, because if I is empty, there does not exist any element k such that bool(k) is true.

all(I)

Return True if all elements of the iterable are true (or if the iterable is empty).

    # [ i is an iterable ->
    #     if (i is empty) or (bool(k) is true for all k in i) ->
    #       test  :=  True
    #     else ->
    #       test  :=  False ]
    test = all(i)

Here we see a compound condition: there are two True cases, one case where the iterable is empty, and another case where the iterable is nonempty and all its members are true.

s.islower()

Return True if all cased characters in s are lowercase and there is at least one cased character in s, False otherwise.

    # [ s is a str or unicode value ->
    #     if (s contains at least one cased character) and
    #     (all cased characters in s are lowercase) ->
    #       test  := True
    #     else ->
    #       test  :=  False ]
    test = s.islower()
str.ljust(width[, fillchar])

Return the string left justified in a string of length width. Padding is done using the specified fillchar (default is a space). The original string is returned if width is less than len(s).

    # [ (s is a str or unicode) and (width is an integer) and
    #   (fillchar is a one-character str or unicode, defaulting to
    #   one space in the same type as s) ->
    #     if width < len(s) ->
    #       a  :=  s
    #     else ->
    #       a  :=  s + (len(s)-1 copies of fillchar) ]
    a = s.ljust(width, fillchar)

There are three parts to the precondition. The first two constrain the types of the s and width arguments. The third part constrains both the type and the length of the fillchar argument, and also specifies the default value.

list.reverse()

Reverses the elements of a list in place.

    # [ L is a list ->
    #     L  :=  L with its elements reversed
    #     x  :=  None ]
    x = L.reverse()

The list.reverse() method doesn't return an explicit result, so by the Python convention, if you assign the value of this expression to a variable, that variable is set to None.

list.pop([index])

Remove and return the item at index (default, the last item). Raises IndexError if the list is empty or index is out of range.

    # [ (L is a list) and (i is an int, defaulting to -1) ->
    #     if -len(L) <= i < len(L) ->
    #       k  :=  L[i]
    #       L  :=  L with element [i] removed
    #     else -> raise IndexError ]
    k = L.pop(i)

The two preconditions constrain the types and values of the arguments, and specify the default value of i. Note that this method modifies two state items: it returns a value and it also modifies the original list. The else clause illustrates the special form for cases that raise an exception.

This intended function was written under the assumption that the reader is familiar with the Python convention regarding negative indices: L[-1] is the last element of L, L[-2] is the penultimate element, and so on; in general, for negative k, L[k] is equivalent to L[len(L)+k].

If we were writing the intended function for readers who might not be familiar with that convention, we could be more explicit:

    # [ (L is a list) and (i is an int, defaulting to -1) ->
    #     if 0 <= i < len(L) ->
    #       k  :=  L[i]
    #       L  :=  L with element [i] removed
    #     else if i < 0 ->
    #       k  :=  L[len(L)+i]
    #       L  :=  L with element [len(L)+i] removed
    #     else -> raise IndexError ]
    k = L.pop(i)