runner.py 文件源码

def _expected_result(self):
        initial = re.compile('INITIAL:?\s*(?P<state>.*)')
        state = re.compile('STATE:?\s*(?P<state>.*)')
        loop = re.compile('LOOP:?\s*(?P<state>.*)')
        final = re.compile('FINAL:?\s*(?P<state>.*)')
        for token in tokenize.tokenize(io.BytesIO(self.source.encode('utf-8')).readline):
            if token.type == tokenize.COMMENT:
                comment = token.string.strip("# ")
                initial_match = initial.match(comment)
                state_match = state.match(comment)
                loop_match = loop.match(comment)
                final_match = final.match(comment)
                if initial_match:
                    result = initial_match.group('state')
                    line = -inf                 # -inf for a precondition
                    yield line, result
                if state_match:
                    result = state_match.group('state')
                    line = token.start[0]
                    yield line, result
                if loop_match:
                    result = loop_match.group('state')
                    line = -token.start[0]      # negative line number for a loop invariant
                    yield line, result
                if final_match:
                    result = final_match.group('state')
                    line = inf                  # inf for a postcondition
                    yield line, result