Take a look at Frama-C or Ada Spark sometime; they apply the predicate transformer semantics style to code and do pretty well. But yeah, incomplete specificatio

Take a look at Frama-C or Ada Spark sometime; they apply the predicate transformer semantics style to code and do pretty well. But yeah, incomplete specifications are always fun.