The material in these lecture notes offers an exposition - aimed at graduate students rather than resemrchers in ~he field - of a topic often called "program schemata" or "schematology" The subject matter represents one approach to forrealizing the elusive notion of the "semantics of programming languages". The idea is to model an "abstract flowchart" and study the interrelation between the syntax of programs (what can be said about their behavior from their format) and the semantics (what they actually "do", depending on the interpretation, the programme language, and perhaps even the implementation) and examine the application of formal proof systems to verify properties of programs.