Inferring Formal Software Specifications from Episodic Descriptions

Abstract

The WATSON automatic programming system computes formal behavior specifications for process-control software from informal scenarios: traces of typical system operation. It first generalizes scenarios into stimulus-response rules, then modifies and augments these rules to repair inconsistency and incompleteness. It finally produces a formal specification for the class of computations which implement that scenario and which are also compatible with a set of domain axioms. A particular automaton from that class is constructed as an executable prototype for the specification. WATSON's inference engine combines theorem proving in a very weak temporal logic with faster and stronger, but approximate, model-based reasoning. The use of models and of closed-world reasoning over snapshots of an evolving knowledge base leads to an interesting special case of non-monotonic reasoning.