This rule is for performing some operation on every element of
a Python iterable (sequence value), typically in a
for statement with this general form.
S: # [
The proof rule is in two parts.
Sis empty, does doing nothing have the same net effect as intended function
Sis nonempty, does doing intended function
Bto the first element of
S, followed by doing intended function
Ato the remaining elements of
S, have the same net effect as intended function
Aon the entire sequence
Here's an example. This function implements the logic of
str.join() method, the equivalent of
def joiner(connector, pieceList): '''Join the pieces of pieceList with the connector. [ (connector is a string) and (pieceList is a list of strings) -> return a string containing the elements of (pieceList) separate by (connector) ] ''' #-- 1 prefix = '' result = '' #-- 2 # [ if pieceList is empty -> # I # else -> # result := result + prefix + (elements of (pieceList), # separated by (connector) # prefix := connector ] for piece in pieceList: #-- 2 body # [ result := result + prefix + piece # prefix := connector ] result = result + prefix + piece prefix = connector #-- 3 return result
Let's apply the two proof rules to this example.
pieceList is an empty
sequence. In that case, the
for loop never
executes, so the return value is the value of
result set in prime #1, the empty string. The
overall intended function specifies that the connector is
inserted only between elements; since there are no elements,
the empty string is the correct result value.
In the case that
pieceList is not empty,
we apply the second proof rule. After applying the #2 body
result is set to the first
prefix is set to the value of
We then apply the intended function for the entirety of prime #2. After that, the states of our two variables are:
result is the first element of
pieceList, followed by the value of
prefix (which is now a copy of
connector), followed by the remaining elements
pieceList separated by
prefix is set to a copy of
So in the case that
pieceList is nonempty,
the net changes are exactly what the intended function for
joiner function specifies.
Note that primes #1 and #3 have no intended functions. In these cases, the code itself serves as the intended function. This is acceptable only when the meaning is quite clear. For example, the intended function for prime #1 would be:
#-- 1 # [ prefix := an empty string # result := an empty string ] prefix = '' result = ''
Assuming that the reader knows that
'' is the
empty string in Python, the comment becomes pretty much