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.
True if any element of the
is true. If the iterable is empty, return
# [ 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
is empty, there does not exist
k such that
bool(k) is true.
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.
True if all cased characters in
s are lowercase and there is at least one
cased character in
# [ 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()
Return the string left justified in a string of length
. Padding is done using the specified
is a space). The original string is returned if width is
# [ (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
arguments. The third
part constrains both the type and the length of
argument, and also specifies the default value.
Reverses the elements of a list in place.
# [ L is a list -> # L := L with its elements reversed # x := None ] x = L.reverse()
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
Remove and return the item at
(default, the last item).
IndexError if the list is empty or
# [ (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
. 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
is the penultimate element, and so on; in general, for
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)