Flowcharts and Machines

Abstract

Flowcharts are a common tool for describing everyday algorithms. Most computer programming languages admit flowchart programming. Also several definitions of computability use models based on the concept of flowchart. In this chapter general definitions of flowcharts and machines (machine := flowchart + input encoding + output encoding) and their semantics are given. Two very useful basic transformations for flowcharts, simulation and refinement, which we shall use repeatedly in later proofs, will be introduced and proved to be correct. Finally the change of input and output encoding is considered. The aim of this chapter is to give a framework for formulating several later proofs more rigorously and transparently and in addition to supply a precise method for developing programs together with correctness proofs. Roughly speaking, a flowchart is a list of operations and tests (called statements) on a dataset D, where the order of execution is determined by a finite table. Before defining a certain class of flowcharts formally we explain the idea by an example.