Logical Theories for Representing Flowchart Schemata.

摘要

The looping structure of flowchart schemata is investigated using a class of two sorted languages called Function Iteration Languages,or FILs. A formula in the interpreted theory corresponding to a FIL is said to represent a flowchart schema if and only if the models in which the formula is valid correspond precisely to the interpretations in which the schema halts. It is shown that the first order functional calculus suffices to represent only non-looping schemata. It is further shown that as the power of the second sort theory of the FIL is increased,the class of flowchart schemata represented in the theory corresponding to the FIL grows larger. A proper extension of Paterson's class of non-intersecting loop schemata is shown. . . . etc. (Author)