Translatability and Decidability Questions for Restricted Classes of Program Schemas

Two new classes of schemas are introduced: the reachable schemas and the semifree schemas. A schema is reachable if every statement in the schema is executed under some interpretation. A schema is semifree if every test in the schema is necessary in the sense that each exit of the test is taken under some interpretation. It is shown that most of the standard decision problems are unsolvable for schemas in these two classes, and that there can be no algorithm which effectively translates an arbitrary schema into an equivalent reachable or semifree schema, even though such equivalent schemas always exist. These classes are also compared to the free and liberal schemas, and interclass translatability questions are investigated. It is demonstrated that every reachable schema can be effectively translated into a semifree schema, even though it is not decidable whether a reachable schema is semifree.