STG: a tool for generating symbolic test programs and oracles from operational specifications