Checks/generates verification conditions for SE 212.

vc_checker.py

#!/usr/bin/env python3

import fileinput
import re
import sys

def parse():
    mode = 'start'
    prev_line = ''
    conc_next = False
    vcs = []
    proofs = []
    assert_re = re.compile('assert\(([^%]+)\);')
    for line in fileinput.input():
        if mode == 'start' and "#check PC" in line:
            mode = 'proc'
        elif mode == 'proc':
            if "#check ND" in line:
                mode = 'proofs'
            elif "(VC " in line:
                prev = assert_re.search(prev_line)
                if prev:
                    premise = prev.group(1)
                else:
                    premise = None
                conclusion = assert_re.search(line).group(1)
                vcs.append((premise, conclusion))
        elif mode == 'proofs':
            if line.strip() == '|-':
                conc_next = True
                continue
            elif conc_next:
                proofs.append((prev_line.strip(), line.strip()))
                conc_next = False
        prev_line = line
    return vcs, proofs

if __name__ == "__main__":
    vcs, proofs = parse()
    if proofs:
        if len(vcs) != len(proofs):
            sys.exit("ERROR: number of VCs does not match number of proofs")
        for i, ((p1, c1), (p2, c2)) in enumerate(zip(vcs, proofs)):
            if p1 and p1 != p2:
                sys.exit("ERROR: VC {}:\n{}\ndoes not match\n{}".format(i+1, p1, p2))
            if c1 != c2:
                sys.exit("ERROR: VC {}:\n{}\ndoes not match\n{}".format(i+1, c1, c2))
    else:
        for i, (p, c) in enumerate(vcs):
            print("% VC {}\n".format(i+1))
            print("#check ND\n")
            print("{}\n|-\n{}\n".format(p if p else '???', c))