Let P be a program component that reads a list of N records and a range condition on the record key. The first seven characters of the record fonn the record key. P reads the key and produces an output file that contains only those records whose key falls in the prescribed range. For example, if the range is "JONES" to "SMITH," then the output file consists of all records whose keys are lexicographically between "JONES" and

"SMITH." Write the input and output conditions as assertions to be used in proving P correct. Write a flow diagram of what P's logical flow might be and identify the transformation points.